{"id":"dfa7d148-94f3-409c-986d-d56135288e02","arxiv_id":"2606.12594","paper_version":1,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Pythagoras-Prover family achieves 93.0% on MiniF2F-Test with a 32B model and has its 4B version surpass a 671B prior model at pass@32, using ALF data augmentation and curriculum training.","lead":"Pythagoras-Prover introduces smaller autoregressive and diffusion-based models for Lean theorem proving trained via curriculum SFT and Augmented Lean Formalisation to expand scarce verified data. If the efficiency gains hold, formal proving could become practical on modest hardware.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"Unverified ALF mutations risk supplying invalid or semantically altered training examples","rationale":"The reader's weakest_assumption directly identifies the same unverified-mutation risk. Because the original review was abstract-only, no stronger internal inconsistency can be diagnosed from the supplied text; the concern remains the primary untested link between ALF and the reported gains.","tokens_in":1897,"tokens_out":350,"duration_ms":9574,"concrete_test":"Draw a random sample of 200 statements from the released MiniF2F-ALF training split; for each, (a) attempt full Lean verification of the mutated statement and (b) compare its proof obligations and semantics against the original via type-checking and manual inspection. If >3% fail verification or exhibit changed meaning, re-train the 4B model on the verified subset only and re-evaluate pass@32 on MiniF2F-Test.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The headline performance claims (4B model beating 671B at pass@32; 32B at 93.0% MiniF2F-Test) rest on curriculum SFT that incorporates ALF-generated variants. ALF produces mutated formal statements via self-distillation without Lean verification for every instance, relying only on the claim that perturbations \"preserve their formal character.\" If any non-negligible fraction of these mutations change the theorem's semantics, introduce inconsistencies, or create unsound goals, the training signal becomes noisy; the observed gains could then be artifacts of data contamination or overfitting to surface patterns rather than genuine proof skill. This assumption is load-bearing because the paper positions ALF as the key mechanism for expanding scarce verified data.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The paper introduces Pythagoras-Prover, a family of parameter-efficient Lean theorem provers (autoregressive 4B/32B models and a 4B diffusion model) trained via curriculum SFT on a stratified Lean-verified corpus with dynamic proof filtering. It proposes Augmented Lean Formalisation (ALF) to generate mutated formal statements via self-distillation without per-instance verification, claiming this expands training data while preserving formal character. Key results: the 4B model achieves 86.1% pass@32 on MiniF2F-Test (surpassing DeepSeek-Prover-V2-671B's 82.4%), the 32B reaches 93.0% (open-source SOTA) and solves 93/672 PutnamBench problems; a new MiniF2F-ALF benchmark is released where all models drop in accuracy.","tokens_in":2082,"tokens_out":634,"duration_ms":10920,"significance":"If the performance claims and ALF validity hold, the work demonstrates that smaller models can outperform much larger ones on formal proving benchmarks through data augmentation and curriculum training, advancing practical compute-efficient provers. The release of MiniF2F-ALF as a contamination-sensitive test set and the open-source models are concrete strengths that enable further verification of the results.","major_comments":[{"comment":"Abstract and ALF description (likely §3): the central training pipeline relies on the unverified claim that ALF self-distilled mutations 'preserve their formal character' and logical validity without Lean checking every instance. No empirical validation (e.g., manual audit rate, semantic equivalence checks, or error analysis on a sample of mutations) is reported, which directly undermines the claim that the observed gains reflect improved proof skill rather than noisy or invalid training signal.","section":"Abstract / ALF section"},{"comment":"Experimental results (likely §4, Table on MiniF2F-Test): headline numbers such as 86.1% (4B) and 93.0% (32B) at pass@32 are presented without run-to-run variance, statistical tests, exact train/eval splits, or confirmation that ALF mutations were excluded from evaluation data. This makes it impossible to assess robustness of the comparison to DeepSeek-Prover-V2-671B.","section":"Experimental results section"}],"minor_comments":[{"comment":"The diffusion-based 4B prover is mentioned as a proof-of-concept but receives little quantitative comparison to the autoregressive models; clarify its role and results relative to the main claims.","section":"Model description"},{"comment":"Notation for pass@k and context-length filtering could be made more precise with explicit equations or pseudocode.","section":"Training methodology"}],"recommendation":"major_revision","confidential_remarks":"The soundness concern around ALF is the primary load-bearing issue; if authors can supply verification statistics or a verified subset, the paper would be substantially stronger. No obvious citation or scope issues."},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for the constructive feedback. We address each major comment below with clarifications and planned revisions where appropriate.","responses":[{"response":"We acknowledge that the manuscript does not report a quantitative error analysis or manual audit of ALF mutations. ALF generates variants via self-distillation from Lean-verified statements using syntactic perturbations intended to maintain logical structure. To address this, the revised manuscript will add an appendix reporting a manual audit of 200 sampled mutations, including the rate at which they type-check and preserve semantic equivalence under Lean. This will provide empirical support for the training signal quality.","revision_made":"yes","referee_comment":"[Abstract / ALF section] Abstract and ALF description (likely §3): the central training pipeline relies on the unverified claim that ALF self-distilled mutations 'preserve their formal character' and logical validity without Lean checking every instance. No empirical validation (e.g., manual audit rate, semantic equivalence checks, or error analysis on a sample of mutations) is reported, which directly undermines the claim that the observed gains reflect improved proof skill rather than noisy or invalid training signal."},{"response":"The reported figures are from single runs owing to training compute limits. The revised version will explicitly state the train/eval splits, confirm that ALF mutations were generated only from the training corpus (and thus absent from MiniF2F-Test), and note the single-run limitation. We will attempt to add variance from additional runs if resources allow; otherwise the limitation will be stated clearly.","revision_made":"partial","referee_comment":"[Experimental results section] Experimental results (likely §4, Table on MiniF2F-Test): headline numbers such as 86.1% (4B) and 93.0% (32B) at pass@32 are presented without run-to-run variance, statistical tests, exact train/eval splits, or confirmation that ALF mutations were excluded from evaluation data. This makes it impossible to assess robustness of the comparison to DeepSeek-Prover-V2-671B."}],"tokens_in":1663,"tokens_out":452,"duration_ms":14284,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"Pythagoras-Prover reports a 4B autoregressive model reaching 86.1% pass@32 on MiniF2F-Test, ahead of DeepSeek-Prover-V2-671B at 82.4%, while the 32B version hits 93.0% and solves 93 PutnamBench problems. They also introduce a diffusion-based 4B prover that refines proofs iteratively. The training uses curriculum SFT on stratified easy-medium-hard Lean problems, dynamic filtering to keep traces under 8k tokens, and Augmented Lean Formalisation (ALF) that creates statement variants via self-distillation.\n\nThe curriculum and filtering steps are practical for managing long proofs and compute. Releasing MiniF2F-ALF, where every model drops in accuracy, gives a concrete way to check robustness to surface changes. The diffusion prover is a distinct direction from the usual autoregressive setup. These elements are new in combination and the numbers on the standard benchmark are stronger than prior open models of similar size.\n\nThe soft spot is ALF. The method perturbs statements without Lean verification on every instance, counting on the changes preserving formal character. If even a modest fraction of mutations shift semantics or create inconsistent goals, the extra training signal becomes unreliable and the efficiency claims could partly reflect data artifacts. The paper positions ALF as central to expanding scarce verified data, so this needs clearer validation in the full text.\n\nThe work targets people building practical Lean provers under limited compute. It has enough concrete results and method details to merit peer review, with the main request being tighter evidence on ALF data quality.","headline":"The 4B model beating a 671B one on MiniF2F is the real headline, but it depends on ALF mutations that skip full verification.","tokens_in":2553,"tokens_out":407,"would_cite":false,"duration_ms":11472,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"Augmented Lean formalisation lets 4B and 32B models outperform far larger theorem provers on MiniF2F and PutnamBench.","keywords":["Lean theorem proving","formal verification","augmented formalisation","self-distillation","curriculum learning","MiniF2F","PutnamBench","diffusion model"],"falsifier":"Run the trained models on a fresh collection of formally verified mutated statements or on MiniF2F-ALF with every variant manually checked; a sharp drop relative to the reported numbers would indicate the unverified mutations were not supplying reliable signal.","tokens_in":2825,"feed_emoji":"📐","tokens_out":824,"duration_ms":14006,"temperature":0.7,"pith_summary":"The paper presents Pythagoras-Prover, an open-source family of Lean theorem provers designed for modest compute. It combines a stratified verified corpus for curriculum supervised fine-tuning, dynamic trace filtering to fit 8k-token limits, and Augmented Lean Formalisation that creates statement variants through self-distillation without verifying every mutation. The resulting 4B model exceeds a 671B baseline at pass@32 on MiniF2F-Test while the 32B model sets a new open-source record and solves 93 PutnamBench problems. A diffusion-based 4B variant is also tested as an alternative to autoregressive generation. Readers would care because formal proving has required heavy resources; the work shows a route to strong results with smaller models and expanded but partially unverified data.","feed_headline":"4B Lean prover beats 671B model on MiniF2F-Test","feed_subtitle":"Pythagoras-Prover-4B hits 86.1 percent pass@32 using augmented statements and far less compute than larger baselines.","key_machinery":"Augmented Lean Formalisation (ALF), a process that perturbs known formal statements while preserving their formal character and fills the variants with self-distilled proofs to supply extra training signal without full verification of each instance.","core_discovery":"Pythagoras-Prover-4B reaches 86.1 percent pass@32 on MiniF2F-Test, surpassing DeepSeek-Prover-V2-671B's 82.4 percent with roughly 167 times fewer parameters, while Pythagoras-Prover-32B attains 93.0 percent on the same test and solves 93 of 672 PutnamBench problems. These outcomes follow from training on a Lean-verified corpus divided into easy-medium-hard tiers for progressive learning, dynamic proof-reasoning filtering, and Augmented Lean Formalisation that perturbs known statements and populates variants via self-distillation to enlarge the training signal.","pith_inferences":["The same augmentation approach could be applied to other interactive theorem provers beyond Lean to reduce dependence on surface forms of statements.","If the unverified mutations prove reliable across domains, the method could lower the barrier to training formal systems for domains with even scarcer verified data.","Releasing MiniF2F-ALF as a harder benchmark suggests that future work should routinely test on mutated variants to guard against overfitting to surface forms."],"forward_implications":["Curriculum ordering from short simple proofs to longer harder ones allows models to acquire proof skills progressively within fixed context budgets.","Dynamic filtering that keeps only informative traces while respecting token limits makes supervised fine-tuning practical on scarce verified data.","A diffusion-based prover offers an iterative refinement path at inference time that differs from standard autoregressive sampling.","The 32B model remains strongest on the contamination-sensitive MiniF2F-ALF benchmark while the 4B model matches prior state-of-the-art accuracy there."],"fun_headline_variants":["4B beats 671B on MiniF2F-Test","Pythagoras-Prover-4B beats 671B model","32B achieves 93 percent on MiniF2F-Test","ALF augments Lean data without verification"],"cache_read_input_tokens":2112,"weakest_assumption_plain":"Mutated formal statements generated by Augmented Lean Formalisation via self-distillation supply valid and useful training signal even though they are not formally verified for every instance.","fun_headline_variants_meta":{"raw":{"variants":["4B beats 671B on MiniF2F-Test","Pythagoras-Prover-4B beats 671B model","32B achieves 93 percent on MiniF2F-Test","ALF augments Lean data without verification"]},"model":"grok-4.3","cost_usd":0.010146,"raw_usage":{"total_tokens":4607,"prompt_tokens":882,"num_sources_used":0,"completion_tokens":66,"cost_in_usd_ticks":101462000,"prompt_tokens_details":{"text_tokens":882,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":3659,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":882,"tokens_out":66,"duration_ms":18027,"temperature":1.0,"reasoning_tokens":3659,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-06-27T09:54:07.995256+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"Run the trained models on a fresh collection of formally verified mutated statements or on MiniF2F-ALF with every variant manually checked; a sharp drop relative to the reported numbers would indicate the unverified mutations were not supplying reliable signal.","supporting_citations":[],"review_version":1}