PaperlayerView exact revision on arXiv

Source-linked AI summary

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

arXiv:2606.12594v1cs.AI

TL;DR

Lean theorem proving often depends on frontier-scale models or costly inference, limiting practical compute efficiency. Pythagoras-Prover combines staged verified-data training with Augmented Lean Formalisation, and its 4B model reaches 86.1% pass@32 on MiniF2F-Test versus 82.4% for a 671B baseline.

  • Problem

    Strong Lean-proving results typically require very large models or computationally intensive inference, motivating compute-efficient alternatives.

  • Method

    Pythagoras-Prover uses a curriculum-stratified Lean-verified corpus and Augmented Lean Formalisation to expand training data with structured formal variants.

  • Results

    Pythagoras-Prover-32B achieves the strongest reported open-source performance across MiniF2F-Test and PutnamBench, while its 4B model reaches 86.1% pass@32 versus 82.4% for DeepSeek-Prover-V2-671B.

  • Takeaways & Limitations

    The results support that careful data construction and efficient training can partly substitute for raw model scale in Lean theorem proving.

  • Takeaways & Limitations

    ALF variants are not Lean-verified, relying on statement-alignment checks rather than proof-validity certification.

Abstract

from arXiv · show

Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.

1 Introduction

Pythagoras-Prover is presented as a compute-efficient, open-source family of Lean 4 theorem provers that combines smaller models with a compute-frugal data and training pipeline. Its approach includes curriculum learning, Augmented Lean Formalisation, dynamic reasoning filtering, and autoregressive and diffusion-based generation.

  • Compute-efficient provers: 86.1% vs 82.4% at pass@32 on MiniF2F-Test: Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B while using roughly 167× fewer parameters.The comparison is reported despite the 4B model being approximately 167× smaller.
  • Compute-frugal data pipeline: Roughly 800K Lean-verified instances are stratified into easy, medium, and hard tiers for curriculum supervised fine-tuning.The curriculum progresses from shorter, simpler proofs to longer, more difficult ones.
  • Compute-efficient provers: The released family spans autoregressive Lean provers at 4B and 32B parameters and a 4B diffusion-based proof-of-concept model.The diffusion model is described as a first proof-of-concept diffusion-based theorem-proving model.
  • Compute-frugal data pipeline: ALF expands the verified corpus by roughly 2.5× using structured mutations and lightweight sanity checks rather than Lean verification for every mutated instance.Applying the same mutation operator to MiniF2F-Test produces MiniF2F-ALF for probing transfer across nearby formal variants.
  • Efficient adaptation recipe: Dynamic proof–reasoning filtering preserves informative traces while keeping each supervised-fine-tuning instance within an 8K-token context budget.The adaptation recipe combines parameter-efficient supervised fine-tuning, curriculum learning, self-distillation, and reinforcement learning from Lean verification.

2 Methodology

Pythagoras-Prover uses a Lean-gated, difficulty-stratified data pipeline followed by curriculum SFT, reinforcement learning, and ALF-based continued training. Its ALF and diffusion components expand training data efficiently while distinguishing statement alignment from formal verification and masking complete Lean tactics during diffusion training.

  • Seed corpus: Easy and medium instances follow a three-stage pipeline of formal statement synthesis, formal proof verification, and rubric-guided distillation.The rubric targets specific Lean failure modes when generating simplified variants of rejected problems.
  • Initial model training: The training process combines difficulty-ordered curriculum SFT, reinforcement learning on held-out hard problems, and continued SFT on ALF self-distillation data.SFT uses LoRA with an 8,192-token context length.
  • ALF self-distillation: ALF replaces per-instance Lean verification with a single statement-alignment check, reducing the pipeline’s dominant computational cost while sacrificing formal certification of generated proofs.The check confirms that a proof addresses the intended goal but does not establish validity.
  • ALF self-distillation: Approximately 2M filtered ALF and reinforcement-learning proofs form a corpus roughly 2.5× the seed size for continued SFT and diffusion-prover training.ALF data is not Lean-verified because its statement-alignment check confirms relevance but never invokes the Lean type-checker.
  • Diffusion training: The diffusion prover masks complete Lean tactics rather than individual tokens, allowing arbitrary-order filling, revision of earlier commitments, and recovery of whole proof steps.Tactic-level masking strictly generalises token-level masking and prevents exploiting sibling tokens within one tactic.

3 Experimental Setup

The experiments evaluate Pythagoras-Prover on MiniF2F, PutnamBench, and the newly introduced MiniF2F-ALF benchmark, using a standardized Lean-based protocol. MiniF2F-ALF applies controlled statement mutations to probe contamination sensitivity, while retained statements are checked for Lean well-formedness.

  • Benchmarks: The evaluation covers MiniF2F, PutnamBench, and MiniF2F-ALF across differing difficulty and topical coverage.MiniF2F-ALF reuses the ALF mutation operator on the MiniF2F test set.
  • Benchmarks: 488 MiniF2F statements span validation and test splits, with MiniF2F-Test using the Kimina-revised release and corrected erroneous statements.The benchmark contains 244 validation and 244 test statements drawn from high-school competitions.
  • Benchmarks: 672 PutnamBench problems target college-level mathematics from the 1962–2023 Putnam Competition across seven mathematical areas.The listed areas are algebra, analysis, number theory, geometry, combinatorics, probability, and set theory.
  • Benchmarks: 244 MiniF2F-Test statements are mutated into MiniF2F-ALF, producing a 488-statement benchmark for contamination-sensitive evaluation.The construction combines ALF mutations with numerical and variable perturbations, and retained statements are verified as well-formed Lean theorems.
  • Evaluation protocol: Lean 4.9.0-rc1 is used for evaluation, with a 30,000-token maximum generation length and correctness requiring error-free compilation, no unproved goals, and verbatim inclusion of the target statement.The stated correctness conditions include excluding sorry, admit, and otherwise unproved goals.

4 Experimental Results

Pythagoras-Prover achieves leading MiniF2F-Test and PutnamBench results at modest scale, remains robust under ALF perturbations, and demonstrates viable diffusion-based Lean proof generation. Its 4B model exceeds much larger baselines at pass@32, while the 32B model leads on MiniF2F-ALF and PutnamBench.

  • MiniF2F-Test: 93.03% at pass@2048 makes Pythagoras-Prover-32B the highest reported MiniF2F-Test pass rate, exceeding Goedel-Prover-V2-32B’s 92.2% at pass@8192 with one-quarter the sampling budget.The result requires neither inference-time self-correction nor test-time reinforcement learning.
  • PutnamBench: 93 problems at pass@2048 gives Pythagoras-Prover the best open-source PutnamBench result, surpassing Goedel-Prover-V2’s 86 at pass@184 with self-correction.At pass@32, Goedel-Prover-V2 with self-correction solves 57 problems versus Pythagoras-Prover’s 48, but independent restart sampling scales with budget.
  • MiniF2F-ALF: 85.0% is Pythagoras-Prover-32B’s MiniF2F-ALF pass rate, the highest among evaluated models, while every model loses accuracy under statement-level perturbation.Pythagoras-Prover-4B reaches 83.2%, nearly matching Goedel-Prover-V2-32B’s 83.6%, and degrades 2.9 points versus 4.5 points for Goedel-Prover-V2-32B.
  • Pythagoras-Prover-Diffusion: 63.25% with a block size of 32 shows that Pythagoras-Prover-Diffusion can generate Lean proofs through diffusion-style iterative refinement, though it trails Pythagoras-Prover-4B’s 86.1% by roughly 23 points.The authors present this as an existence proof because random masking, limited stable context, and scarce diffusion-suitable Lean data constrain performance.

5 Analysis

The analysis shows that rubric-guided synthesis substantially improves verification yield, Pythagoras-Prover scales strongly on MiniF2F, and MiniF2F-ALF exposes failures hidden by the original benchmark. Diffusion decoding trades 22.7 points of accuracy for 2.58× throughput and a 1.89× throughput-weighted advantage.

  • 5.1 Dataset decomposition: 262,247 of 331,069 easy-tier candidates pass Lean verification (79.2%), a 51.1-point gain over the seed rate of 28.1%.The seed contains 239,824 verified instances out of 852,641 (28.1%).
  • 5.2 Scaling study: 93.03% at pass@2048: Pythagoras-Prover-32B leads all non-self-correcting methods and surpasses self-correcting Goedel-Prover-V2-32B from roughly pass@256.The comparison spans budgets N ∈{32, . . . , 2048} on MiniF2F.
  • 5.3 Per-instance behaviour: 83.20% of original MiniF2F problems are solved by all four representative models, leaving 9.02% unsolved by every system.Only 41/244 problems have at least one failure, while 22/244 are failed by all four models.
  • 5.3 Per-instance behaviour: 13.93% (68/488): MiniF2F-ALF raises the all-model failure rate from 9.02% and expands the at-least-one-wrong set to 18.24% (89/488).Failures diversify across domains, including AMC (30.34%), IMO (24.72%), and MathD (20.22%).
  • 5.4 Diffusion versus autoregressive proving: 22.7 points: autoregressive pass@32 accuracy reaches 86.1% versus 63.3% for Pythagoras-Prover-Diffusion-4B under matched hardware and evaluation.Both systems use the same self-distillation corpus and identical harness, isolating decoding regime.
  • 5.4 Diffusion versus autoregressive proving: 2.58× faster: diffusion produces 10.56 versus 4.10 output tokens per second per GPU worker, yielding a 1.89× throughput-weighted advantage.The throughput-weighted scores are 6.68 for diffusion and 3.53 for autoregressive decoding; the score is a coarse proxy dominated by throughput.

6 Related Work

Related work spans advances in LLM reasoning through chain-of-thought and long-trace reasoning models, alongside formal theorem proving that grounds reasoning in verified proofs. Formal approaches explore multiple proof trajectories using search-based methods such as Monte Carlo Tree Search and breadth-first search.

  • LLM reasoning: LLM reasoning has advanced on complex mathematical tasks through chain-of-thought reasoning and large reasoning models that generate long traces.These models are further enhanced with techniques including confidence selection and iterative refinement.
  • Formal theorem proving and autoformalisation: Formal reasoning grounds LLM reasoning in formal proofs, distinguishing it from general informal reasoning.The passage frames formal theorem proving and autoformalisation as promising directions for this grounding.
  • Formal theorem proving and autoformalisation: Formal theorem-proving systems use Monte Carlo Tree Search or breadth-first search to explore multiple proof trajectories.These methods support iterative proof-search processes.

7 Limitations and Future Work

The paper identifies diffusion-based formal proving as a key future direction, despite the current model trailing its autoregressive counterpart. Future work should scale diffusion to longer effective contexts and hybridize parallel diffusion refinement with autoregressive methods.

  • Diffusion-based formal proving: Diffusion-based proving currently trails its autoregressive counterpart.This is presented as a current limitation of Pythagoras-Prover-Diffusion.
  • Diffusion-based formal proving: Iterative refinement makes diffusion models a promising direction for formal proving and an architectural shift for LLM reasoning.The paper motivates this direction through diffusion’s iterative-refinement mechanism.
  • Diffusion-based formal proving: Future work should scale diffusion to longer effective contexts and hybridize parallel diffusion refinement with autoregressive generation.These extensions are proposed to advance the diffusion-based proving regime.

8 Conclusions … A.4 ALF Self-Distillation

Pythagoras-Prover combines compute-efficient Lean proving with staged data construction, ALF augmentation, and robustness-focused evaluation. The appendices specify synthetic-data generation, semantic deduplication, benchmark decontamination, and ALF self-distillation procedures.

  • 8 Conclusions: Pythagoras-Prover spans 4B and 32B autoregressive models plus a 4B diffusion-based Lean prover, showing strong proving need not require frontier-scale models.The 4B model outperforms a 671B-parameter prover on MiniF2F-Test while being roughly 167× smaller.
  • 8 Conclusions: A staged pipeline extends Lean-verified data, stratifies problems by difficulty, and trains models progressively through easy, medium, and hard proof tasks.Augmented Lean Formalisation expands the verified corpus into diverse formal variants for self-distillation and robustness evaluation.
  • 8 Conclusions: MiniF2F-ALF evaluates transfer beyond exact benchmark memorisation, and contemporary provers lose accuracy on its structured formal variants.The result suggests that high MiniF2F-Test accuracy does not yet guarantee robust transfer to perturbed statements.
  • 8 Conclusions: Careful data construction and efficient training can partly substitute for raw model scale in Lean theorem proving.This conclusion is presented as the paper’s central premise.
  • A.1 Rubric Distillation Prompt: Rubric distillation converts failed Lean proofs into self-contained synthetic mathematics problems with step-by-step solutions and strictly formatted JSON outputs.The generator identifies root-cause errors, classifies them under an extraction rubric, and emits the synthetic question with its solution.
  • A.2 Similarity Filtering for Intra-corpus Deduplication: Easy-tier deduplication uses 3,584-dimensional normalized embeddings and FAISS retrieval to detect semantic duplicates that surface-form methods can miss.Instances are chunked into 5,000-item blocks with 100-item overlap, and pairs above cosine similarity τ = 0.75 are filtered by source priority.
  • A.3 Dataset Decontamination Sweep: Training data undergoes a five-stage decontamination sweep against MiniF2F-Valid, MiniF2F-Test, and PutnamBench, discarding instances when any stage detects a hit.Because MiniF2F-ALF mutates MiniF2F-Test, the first three stages also check 488 mutated ALF statements.
  • A.4 ALF Self-Distillation: ALF self-distillation generates proofs with a post-reinforcement-learning teacher at T = 1.2 and nucleus top-p = 0.95, using completions as training targets.At 2M instances per model, per-sample Lean verification is omitted; Appendix C.2 indicates no material downstream degradation for formal proving.

A.5 Verification of ALF Synthetic Data · A.5.1 Why Self-Distillation? · A.6 Examples of Pythagoras-Prover-Dataset for Each Difficulty

The paper audits a sample of ALF self-distilled instances because verifying all 2M with Lean is computationally prohibitive. It motivates self-distillation as a way to expose the prover to broader proof trajectories when preference-based post-training poorly fits sparse binary verification.

  • A.5 Verification of ALF Synthetic Data: 2M ALF self-distilled instances are computationally prohibitive to verify exhaustively with the Lean compiler.The paper therefore uses a random audit instead of checking the entire corpus.
  • A.5 Verification of ALF Synthetic Data: 2,000 retained ALF instances are sampled uniformly from the final self-distillation corpus for auditing.Each sampled instance is checked under the same Lean environment used for evaluation.
  • A.5 Verification of ALF Synthetic Data: 87.8% of audited ALF instances compile successfully, including each mutated formal statement and its proof.The audit checks complete generated theorems rather than proofs alone.
  • A.5.1 Why Self-Distillation?: After supervised fine-tuning, Pythagoras-Prover already achieves a strong MiniF2F-Test pass rate.The passage frames the remaining improvement opportunity as broader proof-trajectory exposure rather than base capability.
  • A.5.1 Why Self-Distillation?: The remaining headroom is attributed to exposing the model to a wider distribution of proof trajectories.This motivates additional training signal beyond supervised fine-tuning.
  • A.5.1 Why Self-Distillation?: Direct Preference Optimisation is poorly matched to Lean proof training because Lean verification provides only a sparse binary judgement.The derived preference pairs are also described as poorly suited to this regime.

B Experimental Settings … C.2 Decomposition Performance

The experiments use Qwen3-based 4B and 32B models with LoRA fine-tuning, evaluate full pass@N performance and MiniF2F-ALF, and decompose MiniF2F-Test gains from SFT and ALF self-distillation. Pythagoras-Prover achieves strong results across inference budgets, with ALF providing substantial additional improvements.

  • B.1 Training Details: Models use Qwen3-4B and Qwen3-32B backbones, two-epoch rank-64 LoRA applied to all linear layers, and separate SFT, RL, and self-distillation learning rates.The reported learning rates are 3e−4 and 7e−5 for SFT stages and 1e−5 for self-distillation.
  • B.2 MiniF2F-ALF Creation: MiniF2F-ALF mutates all 244 MiniF2F-Test problems by renaming variables while preserving their formal structure and difficulty.The construction targets reduced reliance on memorised surface forms.
  • C.1 Full Pass@N Results: Evaluation reports pass@N across the full tested inference-budget sweep for open-source baselines with and without self-correction.This setup supports comparisons across sampling budgets and inference-time correction strategies.
  • C.1 Full Pass@N Results: At 4B, Pythagoras-Prover reaches 86.1% at pass@32 and 89.8% at pass@2048, exceeding DeepSeek-Prover-V2-671B’s 88.9% at pass@8192.It also reaches 88.1% at pass@1024, while using half the parameters of Goedel-Prover-V2-8B and no inference-time correction loop.
  • C.1 Full Pass@N Results: At 32B, Pythagoras-Prover matches Goedel-Prover-V2-32B at pass@1024 with 92.6% and reaches 93.03% at pass@2048.The 93.03% result surpasses Goedel-Prover-V2-32B’s 92.2% at pass@8192 without iterative repair.
  • C.2 Decomposition Performance: SFT alone yields 79.10% at 4B and 84.02% at 32B on MiniF2F-Test at pass@32.The decomposition treats these results as evidence that the synthetic-data corpus carries most of the signal before later training stages.
  • C.2 Decomposition Performance: ALF self-distillation raises the 4B and 32B results to 86.1% and 89.8%, respectively, producing gains of +6.97 and +5.73 points.These results quantify the additional contribution of ALF beyond supervised fine-tuning.

C.3 Why Long-Context Diffusion Training Destabilises · C.4 Training Performance between full context and dynamic proof-reasoning filtering

C.3 attributes diffusion instability at long contexts to masking-induced gradient variance that scales with sequence length and diverges at low noise, while autoregressive training avoids these terms. C.4 shows dynamic proof-reasoning filtering improves MiniF2F-Test pass@32 at both model scales without changing the training or inference setup.

  • C.3 Why Long-Context Diffusion Training Destabilises: Diffusion loss variance behaves as Var ∝ L(1 −t)/t, although correlated masked-position predictions make this a behavioral scaling rather than an exact variance.The gradient has the same scaling because it uses a 1/t-reweighted sum over masked positions.
  • C.3 Why Long-Context Diffusion Training Destabilises: Doubling context from 4,096 to 8,192 doubles per-step gradient variance, while t →0 creates heavy-tailed contributions under the uniform noise schedule.The larger context also reduces feasible batch size, so fewer samples average the increased per-sequence variance.
  • C.3 Why Long-Context Diffusion Training Destabilises: Tactic-span masking inherits the same L- and t-dependence and amplifies instability by roughly the mean tactic length ¯s.Variable span lengths can increase the variance bound further.
  • C.3 Why Long-Context Diffusion Training Destabilises: The 8,192-token setting destabilises diffusion training but converges cleanly under autoregressive training, whose deterministic loss has neither masking noise nor 1/t reweighting.Figure 10 motivates the 4,096-token budget used for Pythagoras-Prover-Diffusion.
  • C.3 Why Long-Context Diffusion Training Destabilises: Prior masked-diffusion work treats long-sequence stability as variance reduction rather than optimizer-hyperparameter tuning, using shorter contexts, estimators, schedules, or smaller blocks.The shared design pattern is consistent with the reported Pythagoras-Prover-Diffusion observations.
  • C.4 Training Performance between full context and dynamic proof-reasoning filtering: C.4 compares full-context training with dynamic filtering while holding the backbone, synthetic corpus, optimizer, SFT recipe, parameter count, budget, and inference protocol fixed.The only difference is whether reasoning traces are pruned on the fly during training.
  • C.4 Training Performance between full context and dynamic proof-reasoning filtering: +3 solved instances at 4B and +2 instances at 32B are delivered by dynamic filtering on MiniF2F-Test at pass@32.The improvement is reported in a near-saturated benchmark regime, with values given as pass rates and solved counts out of 244.

D Detailed Analysis of MiniF2F

Original MiniF2F-Test failures are concentrated in olympiad-derived AMC and IMO problems, whereas ALF mutation redistributes failures across a broader set of categories. MathD rises to roughly 20% of at-least-one-wrong MiniF2F-ALF instances.

  • Original MiniF2F-Test: AMC and IMO together account for roughly two-thirds of at-least-one-model-wrong failures on original MiniF2F-Test.The analysis covers Pythagoras-Prover-4B, Pythagoras-Prover-32B, Goedel-Prover-V2-8B, and Goedel-Prover-V2-32B.
  • MiniF2F-ALF: Roughly 20% of at-least-one-wrong MiniF2F-ALF instances belong to MathD after ALF mutation.MathD is described as a category of problems imported from MATH.
  • MiniF2F-ALF: ALF mutation breaks the original IMO/AMC concentration, redistributing failures across MathD, Algebra, Number Theory, Induction, and AIME.Each of Algebra, Number Theory, Induction, and AIME occupies a non-trivial share after mutation.

E A Failure Mode of Self-Correction

Self-correction can preserve a flawed logical proof skeleton rather than repair it, causing repeated failure on the Putnam 1966 A4 theorem. Independent restart sampling avoids this failure, while Pythagoras-Prover supplies a valid block-based proof.

  • Failure mechanism: Self-correction loops when the original proof skeleton contains a logical error, whereas independent restarts under the same compute budget recover a valid proof.Error-conditioned refinement repairs mechanical slips but can inherit the same flawed lemma chain.
  • Representative theorem: Pythagoras-Prover successfully proves Putnam 1966 A4, concerning non-square positive integers indexed by closest-square distance.The theorem states a recurrence-defined sequence satisfies a formula involving n + round (Real.sqrt n).

F Effective Token Complexity Calculation

The section introduces effective token complexity (ETC) as an idealised attention-work proxy that accounts for prompt length, generated-token length, and repeated attempts across decoding rounds. Under this approximation, Pythagoras-Prover has roughly 5% lower ETC than Goedel-Prover despite using many more attempts, because Goedel-Prover accumulates much longer contexts.

  • Definition and motivation: ETC estimates idealised attention work for decoding a block of a tokens conditioned on an m-token input.It is proposed because pass@N ignores per-attempt length, while wall-clock cost depends on batching, hardware, and serving infrastructure.
  • Definition and motivation: The linear prompt-attention term and quadratic intra-block self-attention term make the quadratic component dominant when a is comparable to or larger than m.For pass@N, per-attempt ETC is multiplied by N, with multi-round systems summed across rounds.
  • Assumptions and scope: ETC is a worst-case, asymptotic proxy assuming dense global attention in every layer, so it may not represent models using sparse, linear, or gated delta-net attention.The stated scope excludes direct interpretation as realised inference cost for such architectures.
  • Numerical comparison: ≈0.95 ETC_Pythagoras-Prover/ETC_Goedel-Prover, implying roughly 5% lower effective token complexity for Pythagoras-Prover under the approximation.Pythagoras-Prover uses 1024 attempts versus Goedel-Prover’s 184, but each restart has a short input context while Goedel-Prover’s later rounds use longer accumulated contexts.
Loading 2606.12594v1…