{"id":"f0de3216-6a57-42b0-8f75-c2554ff0d93e","arxiv_id":"2502.00212","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":7,"one_line_summary":"A self-play loop in which an LLM generates conjectures graded by its own prover's pass rate doubles the LeanWorkbook solve rate to 28.5% and sets whole-proof-method records on miniF2F (65.0% pass@3200), ProofNet (23.9%), and PutnamBench (8/644).","lead":"This paper trains an LLM to both invent new math problems, which it calls conjectures, and prove them, using the problems it can barely solve as a self-generated training curriculum. It reports doubling the fraction of LeanWorkbook problems solved, from 13.2% to 28.5%, plus record results among whole-proof generation methods on miniF2F, ProofNet, and PutnamBench.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The out-of-domain generalization claim is not yet supported: no statement-overlap analysis between STP's training corpora and the miniF2F-test/ProofNet-test/PutnamBench test sets is reported, so the SOTA and generalization numbers may be inflated by contamination.","rationale":"I read the paper in good faith and agree with the reader that this is a strong empirical methods paper: the headline improvements are backed by machine-checked proofs in Lean and Isabelle, the authors release code, models, and data, and the main ablation (Fig. 4, Right) supports the claim that generated conjectures provide denser training signals than expert iteration. The reader's weakest_assumption focuses on mode collapse of the conjecturer: if generated conjectures stop being novel, valid, and learnable, the self-play loop stalls. That is a real risk, and the paper's own Appendix A.5 documents that early experiments collapsed onto algebraic inequalities, which is why the Wasserstein re-weighting was added. However, mode collapse is partially mitigated by the reported 48 to 58 successful iterations and by the concrete heuristics, and the abstract's 'doubling' claim does not logically require indefinite self-improvement. The concern I find more load-bearing for the central claim is dataset contamination. The paper's SOTA and generalization claims depend on the test sets being disjoint from the training corpora, including the base model's proprietary SFT data, and no overlap analysis is provided. This is a specific, checkable missing support rather than a speculative worry: if overlap exists, the Table 1 row explicitly labeled as out-of-domain becomes invalid, and the pass@3200 gains on miniF2F-test, ProofNet-test, and PutnamBench could be inflated by memorization. The reader did list overlap as one of four conditions in the rationale, so my read partially agrees, but I elevate it to the primary load-bearing concern because it directly protects the headline generalization claim, whereas the mode-collapse concern protects a sustainability claim that is not essential to the abstract's quantitative results. A clean contamination scan would settle the issue: if no overlap is found, the SOTA and generalization claims stand, and the paper should move toward acceptance; if overlap is found, the affected benchmark results must be recomputed on the non-overlapping subset before the claims can be accepted.","tokens_in":23168,"tokens_out":9522,"duration_ms":98300,"concrete_test":"Run a contamination scan between every STP training corpus and every reported test set. Normalize Lean 4 statements by alpha-renaming, pretty-printing, and unfolding top-level definitions, then match miniF2F-test, ProofNet-test, and PutnamBench statements against LeanWorkbook, miniF2F-valid, ProofNet-valid, and the DeepSeek-Prover-V1.5-SFT SFT data using both syntactic normalization and embedding-based near-duplicate search. For any candidate match, manually inspect the natural-language source to decide whether the problems are semantically identical. Report the overlap count and, if any overlap exists, recompute Table 1 and Table 3 pass rates on the non-contaminated subset.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim has two parts: self-play improves LeanWorkbook pass rate over expert iteration, and the resulting model generalizes to benchmarks outside the training corpus. The first part is well supported by the Isabelle scaling experiments with Llemma-7b and by the released verifier-checked proofs. The second part is load-bearing for the headline SOTA claims, and it rests on the unstated assumption that the test sets are disjoint from everything the model saw during training. Section 4.1 states that STP training combines LeanWorkbook, miniF2F-valid, and ProofNet-valid, and that the base model DeepSeek-Prover-V1.5-SFT was itself trained on public and proprietary datasets including LeanWorkbook, miniF2F-valid, and ProofNet-valid. The Table 1 row 'STP (w/o miniF2F-valid, ProofNet-valid)' is meant to demonstrate generalization, but if LeanWorkbook's 89K autoformalized natural-language problems overlap with miniF2F-test or ProofNet-test, that row does not establish out-of-domain generalization. PutnamBench statements may also appear in LeanWorkbook or in the base model's SFT data. The paper reports no exact-match or near-duplicate overlap analysis anywhere, even though it is careful to document other dataset limitations, such as Appendix B.3's manual check that many LeanWorkbook statements are unprovable. Because formal statements can be alpha-equivalent or semantically identical after different encodings, exact-string matching is insufficient; the absence of any contamination check leaves the generalization and SOTA claims conditional.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces STP (Self-play Theorem Prover), a training procedure in which a conjecturer and a prover are iteratively finetuned: the conjecturer proposes new formal statements derived from seed theorems and lemmas, and the prover attempts to prove both the original unproved statements and the generated conjectures; proofs verified by Lean/Isabelle are used to train the prover, while conjectures with low-but-positive empirical pass rates, satisfying elegancy and diversity filters, are used to train the conjecturer. The authors report that with 51.3B generated tokens in Lean, STP proves 28.5% of LeanWorkbook, roughly doubling the prior expert-iteration result of 13.2%, and reports state-of-the-art whole-proof generation results on miniF2F-test (65.0% pass@3200), ProofNet-test (23.9% pass@3200), and PutnamBench (8/644). They also run an Isabelle/Llemma-7b study showing better scaling than expert iteration and parallel sampling, and an ablation showing that final retraining with generated conjectures adds 2-3% on miniF2F/ProofNet compared to retraining only on proved original statements.","tokens_in":23414,"tokens_out":9443,"duration_ms":87865,"significance":"The central empirical claim is significant if it holds: it suggests that self-generated conjectures can provide a sustainable source of training signal for formal theorem proving, addressing the sparse-reward plateau of expert iteration. The paper is careful in several ways: the evaluation is anchored to machine-checked proofs in Lean and Isabelle; code, model, and dataset are released; the LeanWorkbook ceiling is honestly estimated from a 20-statement manual audit; and Table 2 reports an ablation isolating the contribution of generated conjectures. The Isabelle scaling experiments from Llemma-7b provide evidence beyond a single base model. The main reservation is that the out-of-domain and SOTA claims rest on unexamined benchmark overlap with the training data, which needs to be addressed before the generalization claims can be accepted.","major_comments":[{"comment":"The claim in Table 1's footnote 5 that STP 'generalizes to out-of-domain theorems', and the headline SOTA numbers on miniF2F-test, ProofNet-test, and PutnamBench, are not supported because the paper reports no statement-level overlap or near-duplicate analysis between the training corpora (LeanWorkbook, miniF2F-valid, ProofNet-valid, and the base model DeepSeek-Prover-V1.5-SFT's public/proprietary SFT data) and these test sets. Since LeanWorkbook was autoformalized from natural-language math problems and the test benchmarks draw on similar competition/undergraduate sources, exact-match and semantic-equivalence duplication could inflate pass@k numbers; the STP (w/o miniF2F-valid, ProofNet-valid) row does not remove this risk because the base model was still trained on related data. I request an overlap analysis with normalization (alpha-renaming, definition unfolding) and a statement of whether any test statements were excluded from training.","section":"Section 4.1, Table 1, Section 4.2"},{"comment":"The robustness of the self-play curriculum is not fully demonstrated: Appendix A.5 discloses that early experiments collapsed onto algebraic-inequality conjectures, and the Wasserstein re-weighting was added to counteract this. The paper does not ablate this re-weighting, the elegancy filter, the pass-rate window (0, 1/4], or the number K of proof samples, so it is unclear whether the improvement over expert iteration comes from the self-play loop itself or from these hand-designed diversity heuristics. Because the central claim is that conjecturing sustains improvement over many iterations (48 in Lean, 58 in Isabelle), please provide an ablation without the Wasserstein re-weighting (or with a weaker diversity regularizer) and report how quickly mode collapse occurs; this would substantially strengthen the claim.","section":"Section 3.2, Appendix A.5, Table 2"}],"minor_comments":[{"comment":"In the sentence 'See Appendx B.1', 'Appendx' is a typo for 'Appendix'.","section":"Section 4.4"},{"comment":"The text says 'we sample K = 32proofs per conjecture/statement'; there is a missing space before 'proofs'.","section":"Section 4.1"},{"comment":"The caption says 'our model is not trained on miniF2F valid', but Section 4.1 states that the Lean experiments combine LeanWorkbook, miniF2F-valid, and ProofNet-valid; please clarify that this caption refers to the Isabelle experiment, or specify the exact training data for that figure.","section":"Figure 4 (Middle) caption"},{"comment":"Please state explicitly which expert-iteration variant (vanilla or optimized) is used for the expert-iteration curve in Figure 2, since Appendix A.6 reports that the two variants have different sample budgets and performance.","section":"Appendix A.6 and Figure 2"},{"comment":"The PutnamBench result of 8/644 problems solved (vs. 6/644 for the prior best method) would be more convincing with an uncertainty estimate or seed variance, since the difference is only two problems on a finite benchmark.","section":"Table 3"}],"recommendation":"major_revision","confidential_remarks":"The missing contamination analysis is the main reason for the major revision recommendation; if the overlap check is clean, the central self-play result appears solid. The paper would also benefit from a robustness ablation of the Wasserstein re-weighting, as the disclosed mode-collapse in Appendix A.5 makes that component load-bearing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should read this one. It's a solid empirical methods paper on self-play for LLM theorem proving, and the core claim holds up: a conjecturer trained to produce problems the current prover can barely solve gives a denser training signal than expert iteration, and the released model, code, and verifier-checked proofs back it up. The LeanWorkbook jump from 13.2% to 28.5% is real, and the Isabelle scaling curves starting from different checkpoints are convincing.\n\nWhat's new: the (0,1/4] pass-rate window as a reward for the conjecturer, the elegancy filter, and the Wasserstein re-weighting to keep conjecture diversity aligned with unproved statements. The paper is honest about the main dataset limitation—a manual audit of 20 unproved LeanWorkbook statements found only 7 provable—and releases artifacts.\n\nSoft spots: the headline comparison uses the vanilla expert iteration baseline; the optimized variant appears only in the appendix, though it's still worse than STP. More importantly, there is no contamination analysis between the training corpora (LeanWorkbook, miniF2F-valid, ProofNet-valid, plus the base model's SFT data) and the test sets. The 'w/o miniF2F-valid, ProofNet-valid' row does not rule out overlap via LeanWorkbook itself or the base model. The SOTA and out-of-domain numbers are conditional until that analysis is done. Also, the core reward thresholds (the 1/4 window, the 20% elegancy quantile) are not ablated. And 'indefinitely' overstates the 48-58 iterations actually run.\n\nNone of this undermines the central result: the self-play curriculum beats expert iteration at equal compute on the training set, and the ablation shows conjectures contribute beyond re-training on proved statements. For anyone working on LLM reasoning or formal math, this is worth the time. For a referee, it's a clear accept-with-revisions: ask for the overlap analysis and ablations, and it's publishable.","headline":"Self-play conjecture generation beats expert iteration in formal theorem proving, but the benchmark claims need a contamination check.","tokens_in":24105,"tokens_out":2673,"would_cite":true,"duration_ms":21388,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Pairing a theorem prover with a conjecturer that generates barely provable statements doubles the fraction of LeanWorkbook provable, from 13.2% to 28.5%.","keywords":["self-play theorem proving","conjecturing","large language models","expert iteration","formal verification","Lean","Isabelle","curriculum learning"],"falsifier":"Count, at each self-play round, the fraction of generated conjectures whose empirical pass rate falls in (0, 1/4] and the number of distinct seed lemmas those conjectures build on; if either number collapses to near zero within a few rounds, the mechanism has stopped generating a curriculum. A simpler decisive test is to give expert iteration the same 51.3B-token budget and the same verifier setting: if it reaches 28.5% on LeanWorkbook without any conjecturer, the conjecturer is not the cause.","tokens_in":22803,"feed_emoji":"🧮","tokens_out":7248,"duration_ms":64384,"temperature":0.7,"pith_summary":"The paper claims that the standard bottleneck in training LLM theorem provers—the scarcity of correct proofs for hard statements—can be sidestepped by having the model generate its own curriculum. STP runs two roles: a prover that attempts proofs and a conjecturer that proposes new statements related to seed theorems, trained on conjectures the current prover can barely prove. Because the conjecturer is rewarded for producing statements with positive but low proof success rates, the loop continuously raises the difficulty of the generated problems and keeps providing dense training signals after expert iteration would plateau. The paper reports that 48 such iterations in Lean prove 28.5% of LeanWorkbook, double the 13.2% of expert iteration, and set whole-proof-generation best results on miniF2F-test, ProofNet-test, and PutnamBench.","feed_headline":"AI that writes its own math exercises doubles theorem-proving score","feed_subtitle":"A conjecturer-prover loop generates barely provable problems, lifting proofs from 13.2% to 28.5% on LeanWorkbook.","key_machinery":"The engine is the conjecturer's reward: a generated statement is kept for training only if the prover's empirical pass rate lies strictly between 0 and 1/4, the proof uses the suggested lemma, and the statement survives an elegancy filter that removes conjectures whose shortest proof is too short relative to the conjecture length. A Wasserstein re-weighting then matches the selected conjectures to the distribution of still-unproved dataset statements, preventing mode collapse onto one topic. This pass-rate window creates an automated curriculum: the conjecturer is always trained on problems that are just beyond the prover's current reach.","core_discovery":"The central discovery is that the sparse-reward plateau in LLM theorem proving can be broken by making the model its own source of new problems. STP trains two roles, a conjecturer and a prover; the conjecturer receives as training data conjectures that the current prover can prove with empirical pass rate in the interval (0, 1/4], together with elegancy and diversity filters, which pushes it to emit statements that are related to, but harder than, the seed theorems. The prover is trained with standard expert iteration on the proofs of those conjectures. Run for 48 iterations in Lean with 3.6M generated conjectures, 241M generated proofs, and 51.3B generated tokens, the loop proves 28.5% of LeanWorkbook, doubling the 13.2% achieved by expert iteration, and reaches 65.0% on miniF2F-test at pass@3200.","pith_inferences":["A testable extension: if the same pass-rate window and Wasserstein re-weighting are applied to natural-language math problems, the loop should sustain improvement in non-formal reasoning as well, since the difficulty signal only needs a pass/fail oracle.","The embedding cosine-similarity cost used for re-weighting anchors the curriculum to the current model's hidden-state geometry; replacing it with a topic-labeled distance would test whether the diversity gain is semantic or merely representational.","If the loop generalizes, it suggests a route toward more open-ended theorem proving without new human data: the conjecturer's job is to keep the prover inside the zone of barely provable statements, where gradient updates are most informative."],"forward_implications":["At the same per-iteration sample budget, the self-play loop continues to add proved statements after expert iteration has flattened, roughly doubling the fraction of LeanWorkbook proved (28.5% vs 13.2%).","Generated conjectures supply a denser training signal: at a checkpoint where unproved dataset statements yielded only 131 correct proofs out of 2.5M sampled, at least 47% of the generated conjectures were successfully proved, so each iteration meaningfully updates the prover.","The final model generalizes beyond its training statements, outperforming prior whole-proof generation methods on miniF2F-test (65.0% at pass@3200), ProofNet-test (23.9%), and PutnamBench (8/644).","Re-training on the generated conjectures, not just on proved dataset statements, contributes a 2–3% gain on miniF2F and ProofNet at pass@128.","In Isabelle, starting from a generic math-focused model, STP scales better than expert iteration or parallel sampling when compared from multiple checkpoints."],"supporting_citations":[{"why":"Provides LeanWorkbook, the de-duplicated 89K-statement formal problem set on which the headline cumulative pass rate is measured.","marker":"[Ying et al., 2024]"},{"why":"Supplies the expert-iteration baseline and the previous 13.2% LeanWorkbook pass rate that STP doubles, along with a tree-search baseline on benchmarks.","marker":"[Wu et al., 2024]"},{"why":"Provides the pretrained prover used as the starting point for the Lean runs and the proof-sampling setup, including temperature and timeouts, that STP inherits.","marker":"[Xin et al., 2024b]"},{"why":"The closest prior self-play conjecturing-and-proving system; the paper contrasts its constrained finite-action-space setting with STP's infinite-action-space, pretrained-model setting.","marker":"[Poesia et al., 2024]"},{"why":"Defines miniF2F, the cross-system olympiad-level benchmark on which STP reports 65.0% pass@3200.","marker":"[Zheng et al., 2021]"},{"why":"Defines ProofNet, the undergraduate-level benchmark on which STP reports 23.9% pass@3200.","marker":"[Azerbayev et al., 2023a]"},{"why":"Defines PutnamBench, the Putnam-competition benchmark on which STP reports 8/644 at pass@3200.","marker":"[Tsoukalas et al., 2024]"},{"why":"Supplies the Lean 4 verifier that defines correctness for the main experiments and is used to extract lemmas for the conjecturer.","marker":"[Moura and Ullrich, 2021]"}],"fun_headline_variants":["Self-play AI writes harder math problems, doubling proof rate","LLM conjecturer-prover loop lifts theorem proving to 65% on miniF2F","Math AI trains on its own conjectures, doubles LeanWorkbook score","Theorem prover that invents its own problems beats expert iteration"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole loop depends on a pretrained model being able to keep inventing fresh, valid, learnable variants of existing theorems—problems the current prover can solve some but not most of the time—for dozens of rounds without the ideas running out or collapsing onto one topic.","fun_headline_variants_meta":{"raw":{"variants":["Self-play AI writes harder math problems, doubling proof rate","LLM conjecturer-prover loop lifts theorem proving to 65% on miniF2F","Math AI trains on its own conjectures, doubles LeanWorkbook score","Theorem prover that invents its own problems beats expert iteration"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000995,"raw_usage":{"total_tokens":4266,"prompt_tokens":1052,"completion_tokens":3214,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":668,"completion_tokens_details":{"reasoning_tokens":3135}},"tokens_in":668,"tokens_out":3214,"duration_ms":22758,"temperature":1.0,"reasoning_tokens":3135,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T19:48:39.153022+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Count, at each self-play round, the fraction of generated conjectures whose empirical pass rate falls in (0, 1/4] and the number of distinct seed lemmas those conjectures build on; if either number collapses to near zero within a few rounds, the mechanism has stopped generating a curriculum. A simpler decisive test is to give expert iteration the same 51.3B-token budget and the same verifier setting: if it reaches 28.5% on LeanWorkbook without any conjecturer, the conjecturer is not the cause.","supporting_citations":[],"review_version":1}