Automated theorem proving sits at an awkward intersection of practical inaccessibility and theoretical importance. Systems like AlphaProof and DeepSeek-Prover-V2 have demonstrated that AI can handle olympiad-level mathematics, but the compute requirements are prohibitive for most researchers. A 671B-parameter model generating thousands of proof attempts is not a tool most labs can deploy. Pythagoras-Prover directly challenges this assumption, showing that careful data construction and training methodology can substitute substantially for raw scale in Lean 4 theorem proving.
The headline result is striking: Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B on MiniF2F-Test at pass@32 (86.1% versus 82.4%), despite using roughly 167 times fewer parameters. The 32B variant achieves 93.0% on MiniF2F-Test at pass@2048, the strongest reported result among open-weight neural Lean provers evaluated without self-correction. These are not marginal improvements squeezed from a saturated benchmark; they represent a meaningful reconfiguration of the accuracy-compute tradeoff that has defined the field.
Key Contributions
The paper makes three distinct contributions that compound on each other:
- A compute-efficient prover family spanning two generation paradigms: autoregressive models at 4B and 32B parameters, and Pythagoras-Prover-Diffusion-4B, presented as the first proof-of-concept diffusion-based theorem-proving model for Lean. The diffusion variant trails the autoregressive 4B model in raw accuracy but generates proofs 2.58 times faster on identical hardware, opening a throughput-oriented point on the accuracy-efficiency frontier.
- Augmented Lean Formalisation (ALF), a structured corpus expansion scheme that produces formal variants of verified statements across five mutation types: simplification, generalisation, lemma proposal, proof-step decomposition, and reformulation. Crucially, ALF uses lightweight structural sanity checks rather than full Lean verification for each mutated instance, decoupling corpus expansion from verifier throughput and achieving roughly 2.5x expansion of the seed corpus.
- MiniF2F-ALF, a companion benchmark derived by applying the same mutation operators to MiniF2F-Test. Every evaluated model loses accuracy on this split, which is a useful diagnostic: it suggests that high pass rates on the original benchmark do not straightforwardly imply generalisation to structurally nearby formal variants.
Methodology
The training pipeline is staged and each stage is motivated by a concrete bottleneck. The starting point is a Lean-verified seed corpus of approximately 800K instances, constructed predominantly using open models with 30B parameters or fewer. This corpus is stratified into easy, medium, and hard difficulty tiers based on proof complexity, enabling curriculum supervised fine-tuning that exposes models progressively to more demanding proof tasks rather than training on a uniform mixture.
During fine-tuning, a dynamic proof-reasoning filtering scheme retains informative reasoning traces while enforcing an 8K-token context budget per instance. This is a practical engineering choice that matters: long reasoning traces are one of the primary cost drivers in formal proof training, and truncating them naively discards useful signal. The filter tries to preserve the most informative portions of each trace within the budget constraint.
ALF then expands the verified seed into structured variants. The key design decision here is the rejection of per-mutation Lean verification. AlphaProof's mutation-based augmentation required Gemini to generate an accompanying proof and the Lean kernel to verify it before any variant could enter training. ALF sidesteps this by operating at the statement level, accepting mutations on structural grounds. The variants are used both as self-distillation targets during post-training and as the basis for MiniF2F-ALF. The same post-training corpus trains both the autoregressive and diffusion provers, enabling a controlled comparison between generation paradigms under matched data conditions.
Reinforcement learning from Lean verification is applied as a final training stage, using the Lean type-checker as the reward signal. This is now a fairly standard component of formal proving pipelines, but the paper's contribution is in what precedes it: the curriculum and ALF expansion reduce the cold-start problem that makes RL from sparse verifier feedback difficult at small model scales.
Results and Scaling Behaviour
The scaling analysis across budgets from pass@32 to pass@2048 reveals something more informative than the headline numbers. Pythagoras-Prover models reach competitive accuracy at small N with shallow improvement slopes thereafter, whereas baselines like DeepSeek-Prover-V2 require much larger sampling budgets to approach comparable performance. This shape indicates that proof-search behaviour has been internalised during training rather than delegated to inference-time search, which is precisely the property relevant to compute-constrained deployment.
Pythagoras-Prover-32B crosses above the self-correction-augmented Goedel-Prover-V2-32B from roughly pass@256 onwards, reaching 93.03% at pass@2048 versus Goedel-Prover-V2-32B's 92.2% at pass@8192. Achieving a stronger result at a quarter of the sampling budget, without any iterative repair loop, is a meaningful efficiency gain.
The MiniF2F-ALF results are worth examining carefully. The benchmark is constructed by applying ALF mutations to MiniF2F-Test statements, and every evaluated model degrades on it. Pythagoras-Prover-32B remains the strongest evaluated prover on this split, while Pythagoras-Prover-4B reaches parity with Goedel-Prover-V2-32B. The degradation pattern across all models suggests that current provers are sensitive to surface-level statement variation in ways that high pass rates on the original benchmark do not reveal. Whether ALF mutations are the right perturbation family to probe this sensitivity is an open question, but the diagnostic value is clear.
The error analysis of rejected seed instances is also informative. Of 612,817 rejected proofs, the dominant failure modes are tactic failures (30.0%, concentrated in linarith, simp, ring, and omega), invalid projection errors (15.2%), and unsolved goals (14.7%). The rubric-guided synthesis strategy that recovers 258,648 of these instances by generating simplified variants is a practical contribution to the problem of Lean data scarcity.
Limitations and Implications
The paper is honest about its limitations. The diffusion prover is explicitly a proof of concept; it trails the autoregressive 4B model in accuracy and the path to closing that gap is not yet clear. The five ALF mutation operators, while already useful, represent a narrow slice of the possible perturbation space. Type-driven mutations, lemma-graph perturbations, and proof-trace mutations are natural extensions that could widen the failure surface exposed by MiniF2F-ALF.
The saturation of MiniF2F is a genuine problem for the field. The paper notes that 83.2% of MiniF2F problems are now solved by all four models in their comparison panel, leaving a residual that is heavily skewed toward AMC and IMO problems. MiniF2F-ALF is positioned as a stronger drop-in variant, but the authors acknowledge that a broader community effort is needed to construct evaluation suites with controlled difficulty stratification. This is not a criticism of the paper; it is an accurate characterisation of where benchmark development needs to go.
The broader implication is that the compute requirements for competitive Lean theorem proving are lower than the current literature suggests. A 4B model trained with careful curriculum design and structured data augmentation can outperform a 671B model at standard inference budgets. This matters for academic labs, for deployment in resource-constrained settings, and for the question of whether formal verification can become a practical component of mathematical AI systems rather than a frontier-only capability.
Models, data, and the MiniF2F-ALF benchmark are released at https://huggingface.co/Pythagoras-LM. The full paper is available at arXiv:2606.12594.