Pith. sign in

REVIEW 4 major objections 6 minor 1 cited by

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper argues that a hybrid pipeline can automatically generate thousands of novel, aesop-unprovable Lean 4 conjectures from Mathlib seeds, and that GRPO training on those conjectures improves theorem proving in targeted domains.

desk verdict A useful synthetic-data generation pipeline with credible counts, but the RL training claim is only in-distribution and the held-out results are flat, so the abstract overstates the case. read the letter →

arxiv 2506.22005 v1 pith:M4AK3AOD submitted 2025-06-27 cs.AI

Naoto Onda , Kazumi Kasaura , Yuta Oriike , Masaya Taniguchi , Akiyoshi Sannai , Sho Sonoda This is my paper
classification cs.AI
keywords Lean4formaltheoremprovingconjecturegenerationGRPOreinforcementlearningMathlibsynthetictrainingdatatopology
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to show that the shortage of formalized training data for theorem provers can be eased by generating conjectures automatically. Its pipeline, LeanConjecturer, takes existing Mathlib files as seeds, uses an LLM to propose new Lean 4 theorem statements, and wraps them in rule-extracted context so they compile. On 40 seed files it reports 12,289 generated conjectures, of which 10,950 parse, 4,130 are novel, and 3,776 cannot be proved by the aesop tactic. The paper then reports that GRPO reinforcement learning on 192 of these conjectures raises proof-attempt success rates and, more modestly, problem-level success, while several generated topology theorems (union properties of semi-open, alpha-open, and pre-open sets) were formally verified. If true, this makes a scalable, domain-directed source of training data available.

What carries the argument

The load-bearing object is the generated Lean 4 conjecture: a theorem statement ending in ':=' with no proof body, paired with the imports and context assembled from the seed file. The machinery has four gates: syntactic validity (Lean parses the statement and only emits a 'sorry' warning), novelty (the exact? tactic finds no existing Mathlib theorem and no earlier generated duplicate), non-triviality (the aesop tactic fails), and iteration (newly accepted statements are fed back as context for the next round). For training, the pipeline adds GRPO with a binary reward (1 for a completed proof, 0 otherwise) on a 7-billion-parameter theorem-proving model, first on 192 interior/closure conjectures and then with 121 semi-open conjectures appended. The "as many as possible" prompt instruction is a key detail: it keeps generation volume independent of seed-file size, producing 412 candidates from a single-theorem file instead of one.

What would settle it

Take the 192 generated conjectures used for training, have an independent verifier determine which are true, and check whether the GRPO-trained model's extra successes are concentrated on those true statements and on previously unsolved problems. If per-problem gains vanish on a fresh set of generated topology conjectures that were not in training, for instance pre-open or regular-open statements, then the central claim that targeted training enhances theorem proving is not supported.

Watch

Extended reading notes

Core claim

On its own terms, the paper's central discovery is that a structured hybrid loop—rule-based extraction of imports, variables, and namespaces from a Mathlib file, plus LLM generation of statement-only hypotheses with the instruction "as many as possible"—yields a large stream of novel, well-typed, aesop-unprovable Lean statements. Running the loop until no new statements appear (or a cap of 15 iterations) produced 12,289 candidates from 40 seeds; after syntax and novelty checks, 4,130 were novel and 3,776 were non-trivial in the sense that aesop cannot close them. Feeding a subset of 192 topology conjectures, later augmented with 121 semi-open set conjectures, into GRPO training of a 7-billion-parameter prover improved proof success from 2,285 to 5,307 successful proofs per 24,576 attempts and per-problem success from 47 to 50 of 192, while a held-out set of 14 alpha-open conjectures showed no clear problem-rate gain. The paper additionally reports verified formal proofs for statements such as the union of two semi-open sets being semi-open, the union of two alpha-open sets being alpha-open, the union of two pre-open sets being pre-open, and the closure of a pre-open set being semi-open.

Load-bearing premise

Everything rests on assuming that training on unverified, possibly false, generated statements makes the prover better at proving other statements, rather than just memorizing the training ones.

Editorial extensions

If this is right

  • Scaling the same loop from 40 seed files to all roughly 6,000 Mathlib files could yield far more than 103.25 novel conjectures per file, since 25 of the 40 files were still producing novel statements when the 15-iteration cap was reached.
  • Targeted GRPO on domain-specific conjectures raises proof success counts within that domain, so a model can be coached on interior/closure and semi-open topology without hand-written training sets.
  • Because conjectures that aesop cannot prove include both true and false statements, the 'non-trivial' filter does not guarantee truth; verification by a separate prover remains necessary before calling a generated statement a theorem.
  • The verified union and closure results for semi-open, alpha-open, and pre-open sets show the pipeline can generate statements that are new formal content, not just syntactic variations of the seed theorems.
  • The small alpha-open transfer gain suggests the learned skill stays close to the training topics, so gains on one topology concept do not automatically move to a neighboring concept.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the real payoff would come from making the truth value of each generated conjecture part of the loop—for example, pairing proof attempts with counterexample search—so false conjectures become disproof training data instead of reward noise.
  • Editorial inference: a natural next experiment is a self-play curriculum that selects 'barely provable' conjectures by current model strength, using a generator like the one in this paper; such a combination is hinted at in the paper's future-work section.
  • Editorial inference: the modest alpha-open transfer suggests testing whether training on a deliberately mixed set of topology concepts (semi-open, alpha-open, pre-open, regular-open) yields problem-rate transfer that single-domain training does not.
  • Editorial inference: the exact?/aesop novelty and triviality checks are themselves a cheap but useful signal; a stronger variant would use the trained prover's own success/failure distribution to define difficulty, making generated corpora self-calibrating.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. The paper introduces LeanConjecturer, a pipeline that combines rule-based context extraction with LLM-based theorem-statement generation to produce Lean 4 conjectures from Mathlib seed files. The pipeline filters statements by syntactic validity, novelty with respect to Mathlib and previously generated conjectures, and non-triviality as measured by failure of the aesop tactic. Over 40 seed files the pipeline reports 12,289 generated conjectures, of which 3,776 are syntactically valid, novel, and aesop-unprovable. The authors then apply GRPO to train DeepSeek-Prover-V2 on 192 generated conjectures about interior and closure operations, later adding 121 semi-open-set conjectures, and report improvements in proof rate and a small improvement in problem rate on the training distribution. A held-out evaluation on 14 alpha-open-set conjectures shows a flat problem rate across checkpoints. The paper also lists several verified theorems about semi-open, alpha-open, and pre-open sets.

Significance. If the generation pipeline is reproducible and the reported counts are accurate, the paper makes a useful engineering contribution to the data-scarcity problem in formal theorem proving: it provides a scalable way to produce syntactically valid, novel, and non-trivially-stated Lean 4 conjectures from existing Mathlib files. The availability of public code and the explicit filtering pipeline are concrete strengths. However, the paper's central claim that GRPO training on these conjectures 'can enhance theorem proving capabilities' is only weakly supported: the main quantitative gains are on the training distribution, and the single held-out evaluation shows no improvement in problem rate. The verified theorems in Appendix A are mostly immediate consequences of the definitions, so the 'mathematical discovery beyond simple variations' framing is not yet established. The contribution is therefore better characterized as a data-generation pipeline with preliminary RL evidence, rather than as a demonstration of enhanced general theorem-proving ability.

major comments (4)
  1. [§4.3, Tables 3–5] The abstract's claim that 'targeted training on domain-specific conjectures can enhance theorem proving capabilities' is not supported by the held-out evaluation. Table 5 shows that on the 14 alpha-open conjectures the problem rate stays flat across checkpoints (9/14, 9/14, 8/14, 9/14) even though the proof rate rises from 466 to 536. With 128 samples per problem, a rising proof rate with a flat problem rate means the model is proving the same problems more reliably rather than solving new ones. This is consistent with overfitting to the training distribution, and it directly undercuts the general-capability claim. The paper needs either additional held-out evaluations on genuinely new problem types or a substantially more cautious statement of what the RL results establish.
  2. [§4.3] The RL training set consists of 192 conjectures used 'without manual filtering, thus including both true and false statements.' Because the reward is binary proof success, false conjectures can never be rewarded, and unproved conjectures of unknown truth contribute only negative or zero reward. The observed proof-rate gain on the training set may therefore reflect memorization of specific statement patterns rather than acquisition of reusable mathematical skill. The paper should either quantify how many of the 192 conjectures were actually proved (and thus are true), filter the training set to conjectures with verified proofs, or discuss more carefully what learning signal the unfiltered set provides.
  3. [§4.4 and Appendix A] The claim that the system 'demonstrat[es] its potential for mathematical discovery beyond simple variations of existing results' is overstated. The theorems listed in Appendix A, such as preopen_empty_set, semi_open_empty, alpha_open_implies_semi_open, and closure_pre_open_is_semi_open, are direct consequences of the definitions and standard library facts; several are proven by aesop or by short simplification chains. These results are better described as automatically generated and verified statements than as mathematical discoveries. The paper should calibrate this language to the actual depth of the verified statements.
  4. [§5.2] The Discussion already concedes that the model 'may not automatically generalize to entirely new problem types within the same domain' and that the alpha-open results 'indicate that while GRPO improves performance on the training distribution, its ability to generalize to novel mathematical concepts requires more sophisticated training strategies.' This concession is in tension with the abstract's unqualified 'enhance theorem proving capabilities.' The abstract and introduction should be revised to state that the improvement is on the training distribution and that generalization to held-out problem types was not observed.
minor comments (6)
  1. [§3.1, Figure 2] The system prompt contains a typo ('F or' instead of 'For') and the formatting of the quoted Lean code block in the prompt is garbled in the manuscript; this should be cleaned up so the prompt is directly usable.
  2. [§4.1] The seed file is referred to as 'InteriorClosureExercise.lean' in Section 4.1 but the URL in Section 3.5 points to 'InterClosureExercise.lean'. Please make the naming consistent.
  3. [Table 1 and Abstract] The abstract says 3,776 conjectures were 'syntactically valid and non-trivial,' but Table 1 shows 10,950 syntactically valid, 4,130 novel, and 3,776 non-trivial. The wording should make clear that the 3,776 are the subset of novel conjectures that aesop cannot prove, not the total number of syntactically valid conjectures.
  4. [§4.3, Tables 3–4] The description of the training schedule is confusing: Table 3 reports 1 and 10 epochs, then the text says 121 semi-open conjectures were added and training continued for 24 more epochs, and Table 4 labels the result '10+24 epochs.' Figure 4 is captioned '34 epochs.' Please state explicitly how many total epochs were run and which checkpoint corresponds to each table row.
  5. [§5.1] The extrapolation from 40 Mathlib files to about 6,000 files assumes that the generation yield per file is independent of file complexity and that the 40 selected files are representative. This assumption should be stated explicitly, since files with more abstract content may produce lower yields.
  6. [Appendix A] Some displayed proofs, especially interior_union_preopen, contain long repetitive tactic chains with many '<;>' repetitions. These proofs are hard to read and may not reflect the actual proof search strategy. It would help to show cleaner proofs or to state that these are raw outputs of the prover.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the generation pipeline is self-contained and the RL generalization limits are explicitly reported.

full rationale

The paper's derivation chain is not circular. Conjecture generation uses Mathlib seed files plus an LLM to produce statements, then applies three independent filters: Lean syntax checking, exact? novelty checking, and aesop non-triviality checking. These filters are operational definitions of 'valid', 'novel', and 'non-trivial' as stated in Section 3.2; they are not equivalent to the paper's output claims that the conjectures are diverse or mathematically interesting. The verified theorems in Appendix A are machine-checked by Lean's kernel, so the claim of 'non-trivial theorems' does not reduce to the input (aesop failure) by construction; rather, the proofs are verified independently of the generator. The GRPO experiments (Section 4.3) report improvement on the training distribution (proof rate 2285 to 5307 per 24576 attempts; problem rate 47 to 50 per 192 problems), which is expected from reinforcement learning on those exact conjectures. However, the paper does not disguise this as a held-out prediction: Table 3 is explicitly labeled 'Proof success rates in the training dataset'. The genuinely held-out alpha-open evaluation (Table 5) shows flat problem rate (9/14 to 9/14 to 8/14 to 9/14), and Section 5.2 explicitly concedes that the model 'may not automatically generalize to entirely new problem types within the same domain'. Thus the broad abstract claim about 'enhancing theorem proving capabilities' is stronger than the evidence supports, but that is an evidence-strength/overclaiming issue, not a circularity issue. There are no load-bearing self-citations, no imported uniqueness theorems, and no fitted parameter relabeled as a prediction. The evaluation on the training set is presented honestly as training-domain performance, and the one out-of-distribution evaluation is reported as a null result rather than claimed as success. Accordingly, no circular step can be exhibited, and the appropriate score is 0.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The pipeline's contribution rests on operational definitions of novelty and non-triviality, on the representativeness of seed files, and on the assumption that RL on generated statements transfers. No new mathematical entities are introduced; SemiOpen, AlphaOpen, and PreOpen are standard definitions reproduced in the appendix.

free parameters (4)
  • Maximum iteration count = 15
    Stops generation; 25 of 40 files were still producing new conjectures when cut off, so total counts depend on this choice.
  • Non-triviality threshold = aesop failure
    A conjecture is called non-trivial if aesop cannot prove it; this operational definition is chosen by hand and does not measure mathematical depth.
  • Sampling attempts per problem = 128
    Problem success rate is defined with 128 proof attempts; larger or smaller samples would change reported rates.
  • GRPO training epochs = 1, 10, and 34
    Reported gains increase with epochs; the paper does not justify early stopping or report variance across runs.
assumptions (4)
  • domain assumption Mathlib seed files are representative enough that LLM variations of them constitute university-level conjectures.
    Generation quality is tied to seed diversity; Section 5.3 admits bias if seeds are not representative.
  • domain assumption Failure of aesop and exact? is a valid proxy for non-triviality and novelty.
    Section 3.2 defines these filters; they are heuristics, not mathematical measures.
  • domain assumption Reinforcement learning on generated statements with proof-success reward improves general theorem-proving ability.
    Section 4.3 tests this, but the only substantial gains are on the training set; held-out alpha-open problems show no problem-rate improvement.
  • domain assumption Lean kernel verification of the generated topology theorems implies they are mathematically meaningful results.
    The theorems are verified, but they are standard properties of semi-open, alpha-open, and pre-open sets, not new mathematics.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving." pith.science (2026). https://pith.science/paper/M4AK3AOD

@misc{pith2026250622005,
  author       = {Pith},
  title        = {Pith review of: LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M4AK3AOD}},
  note         = {Machine review of arXiv:2506.22005}
}
read the original abstract

We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem statement generation, addressing the data scarcity challenge in formal theorem proving. Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial, that is, cannot be proven by \texttt{aesop} tactic. We demonstrate the utility of these generated conjectures for reinforcement learning through Group Relative Policy Optimization (GRPO), showing that targeted training on domain-specific conjectures can enhance theorem proving capabilities. Our approach generates 103.25 novel conjectures per seed file on average, providing a scalable solution for creating training data for theorem proving systems. Our system successfully verified several non-trivial theorems in topology, including properties of semi-open, alpha-open, and pre-open sets, demonstrating its potential for mathematical discovery beyond simple variations of existing results.

Figures

Figures reproduced from arXiv: 2506.22005 by the authors.

Figure 1
Figure 1. Overview of our theorem generation and verification pipeline. The process starts with Mathlib files as input, goes through generation (blue), evaluation (green), and iteration phases, and culminates in verification (red) and reinforcement learning (yellow). The iterative nature of the pipeline allows for continuous generation of novel conjectures while maintaining mathematical validity. 2. Related Work 2.1. Formal T… view at source ↗
Figure 2
Figure 2. System prompt used for theorem generation with LLMs. A key design choice in our prompt is the inclusion of the phrase “as many as possible”. This instruction is crucial for ensuring consistent generation volume regardless of the input file size. Without this directive, we observed that the number of generated conjectures tends to be influenced by the number of theorems in the source Mathlib file, poten￾tially result… view at source ↗
Figure 3
Figure 3. Illustration of novelty assessment using exact? com￾mand with context. By including previously generated conjectures in the context, we can effectively detect and filter out duplicate or similar conjectures, ensuring the generation of truly novel mathe￾matical statements. The iteration process terminates when no new syntactically valid and novel conjectures are generated. However, the “as many as possible” instructi… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Learning curve of GRPO training over 34 epochs. The graph shows the improvement in proof success rates and problem success rates as training progresses. To investigate the generalization capabilities of GRPO train￾ing, we evaluated the model’s performance on a separate…

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis

    cs.AI 2026-04 reject novelty 4.0 of 10

    The paper's claim of pipeline-validated 'major conjecture' discovery is unsupported: the Lean statements are uninterpreted placeholders and the quality scores are self-assigned by the generating model.

Reference graph

Works this paper leans on

9 extracted references · 1 canonical work pages · cited by 1 Pith paper

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    DeepSeek-AI, Liu, A., Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan, C., Dai, D., Guo, D., Yang, D., Chen, D., Ji, D., Li, E., Lin, F., Dai, F., Luo, F., Hao, G., Chen, G., Li, G., Zhang, H., Bao, H., Xu, H., Wang, H., Zhang, H., Ding, H., Xin, H., Gao, H., Li, H., Qu, H., Cai, J. L., Liang, J., Guo, J., Ni, J., Li, J., ...

    arXiv 2025

  3. [3]

    and Ma, T

    Dong, K. and Ma, T. Stp: Self-play llm theorem provers with iterative conjecturing and proving, 2025. URL https://arxiv.org/abs/2502.00212

    arXiv 2025

  4. [4]

    Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification, 2025

    Liu, C., Yuan, Y., Yin, Y., Xu, Y., Xu, X., Chen, Z., Wang, Y., Shang, L., Liu, Q., and Zhang, M. Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification, 2025. URL https://arxiv.org/abs/2506.04592

    arXiv 2025

  5. [5]

    Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z

    Ren, Z. Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z. F., Gou, Z., Ma, S., Tang, H., Liu, Y., Gao, W., Guo, D., and Ruan, C. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL https://arxiv.org/abs/2504.21801

    arXiv 2025

  6. [6]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition, 2024

    Tsoukalas, G., Lee, J., Jennings, J., Xin, J., Ding, M., Jennings, M., Thakur, A., and Chaudhuri, S. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition, 2024. URL https://arxiv.org/abs/2407.11214

    arXiv 2024

  7. [7]

    and Gao, J

    Yin, D. and Gao, J. Generating millions of lean theorems with proofs by exploring state transition graphs, 2025. URL https://arxiv.org/abs/2503.04772

    arXiv 2025

  8. [8]

    Internlm-math: Open math large language models toward verifiable reasoning, 2024

    Ying, H., Zhang, S., Li, L., Zhou, Z., Shao, Y., Fei, Z., Ma, Y., Hong, J., Liu, K., Wang, Z., Wang, Y., Wu, Z., Li, S., Zhou, F., Liu, H., Zhang, S., Zhang, W., Yan, H., Qiu, X., Wang, J., Chen, K., and Lin, D. Internlm-math: Open math large language models toward verifiable reasoning, 2024. URL https://arxiv.org/abs/2402.06332

    arXiv 2024

Show all 9 references
  1. [9]

    M., and Polu, S

    Zheng, K., Han, J. M., and Polu, S. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR. OpenReview.net, 2022. URL http://dblp.uni-trier.de/db/conf/iclr/iclr2022.html#ZhengHP22

    2022

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.