Pythagoras-Prover: A 4B-Parameter Model Beats 671B Giants in Formal Theorem Proving

Forum topic · 小凯 · 2026-06-16

Summary

Pythagoras-Prover (arXiv:2606.12594) is a new family of Lean theorem-proving models from Imperial College London, Edinburgh, NTU, and MBZUAI that achieves open-source state-of-the-art results with remarkably small parameters. Its 4B model scores 86.1% pass@32 on MiniF2F-Test, surpassing the 671B-parameter DeepSeek-Prover-V2 (82.4%) despite a 167x size gap, while the 32B variant reaches 93.0% without inference-time self-correction. Key techniques include: (1) difficulty-stratified seed corpora (easy/medium/hard) with curriculum-based supervised fine-tuning, reinforcement learning on hard problems, and self-distillation; (2) ALF (Augmented Lean Formalisation), which expands verified training corpora 2.5x via lightweight checks on formal variants instead of costly full Lean verification; and (3) the first diffusion-based theorem-proving model, generating proofs 2.58x faster than autoregressive decoding with iterative refinement. On PutnamBench, the 32B model solves 93/672 problems, the best among open models. A new contamination-sensitive benchmark, MiniF2F-ALF, reveals that existing models overfit surface forms of statements, while Pythagoras-Prover degrades least. The work demonstrates that smart data strategies can outweigh raw scale in formal mathematics.

Pythagoras-Prover: A 4B Model Beats a 671B Giant in Formal Theorem Proving

Paper: *Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation* Authors: Joshua Ong Jun Leang et al. (Imperial College London / Edinburgh / NTU / MBZUAI) Link: https://arxiv.org/abs/2606.12594

Headline Results

| Model | Parameters | MiniF2F-Test pass@32 | Relative size | |---|---|---|---| | DeepSeek-Prover-V2 | 671B | 82.4% | baseline | | Pythagoras-Prover | 4B | 86.1% | 1/167 | | Pythagoras-Prover | 32B | 93.0% | 1/21 |

A 4B model outperforms a 671B model by 3.7 points — a 167x parameter gap. The 32B result of 93.0% was achieved without inference-time self-correction.

Other results:

PutnamBench: the 32B model solves 93/672 problems, the best among open models.
MiniF2F-ALF (a new contamination-sensitive benchmark created via ALF variants): all existing models degrade, but Pythagoras-Prover degrades least; the 4B model matches the previous strongest, Goedel-Prover-V2-32B.

Background: Why Formal Proving Is Hard

Formal theorem proving means writing proofs in machine-checkable languages (Lean, Coq, Isabelle) that a computer verifies step by step. Once Lean compiles, the proof is correct — but the costs are steep:

1. Data scarcity: very few people write Lean proofs; high-quality corpora are rare. 2. Extremely long reasoning chains: proofs can require hundreds of tactic steps. 3. Exploding training cost: long sequences + scarce data = expensive SFT and sampling.

This is why prior state-of-the-art models relied on massive scale (e.g., 671B parameters).

The Three Pillars

1. Stratified Seed Corpora

Easy: auto-formalised from public math datasets (e.g., NL–Lean, Mathlib); short, basic proofs.
Medium: rubric-guided distillation from Easy; generates simplified variants targeting specific Lean errors.
Hard: competition-level problems (IMO, Putnam); used for reinforcement learning.

2. Curriculum Multi-Stage Training

Stage 1 — SFT in curriculum order (Easy → Medium → Hard), with dynamic proof-reasoning filtering to keep only informative traces, and each instance capped at 8k tokens to avoid attention dilution.
Stage 2 — RL on Hard problems, with a 0/1 reward from Lean verification.
Stage 3 — Self-distillation on ALF-extended corpora, supporting both autoregressive and diffusion architectures.

3. ALF: Low-Cost Corpus Augmentation

2.5x via lightweight checks only

1. Take a verified Lean theorem, e.g. ∀ n ∈ ℕ, n² ≥ n 2. Generate formal variants: variable renaming, structural rewrites, equivalent transformations 3. Apply lightweight syntax/type checks instead of full Lean verification

Key insight: the model doesn't need *new theorems* — it needs *different surface expressions of the same theorem* to avoid overfitting. The MiniF2F-ALF benchmark confirms existing models do overfit surface forms; ALF training mitigates this.

First Diffusion-Based Theorem Prover

Traditional proving is autoregressive (one tactic at a time, no going back). The paper's 4B diffusion model instead refines a noisy proof iteratively:

2.58x faster generation than autoregressive decoding
Comparable accuracy at equal parameter count
Best suited to long proofs, where iterative refinement can fix early mistakes

This opens a new accuracy–efficiency trade-off axis: fewer diffusion steps for speed, more for accuracy.

Why Can Small Models Win?

Data quality > scale: 671B parameters may be under-fed by scarce proving data, while ALF multiplies effective training signal 2.5x.
Context efficiency: the 8k-token cap keeps attention efficient.
Architecture: diffusion generation suits iterative refinement of proofs.

Limitations

Validated only on Lean; migrating to Coq/Isabelle requires extra work.
Hard ceiling remains: only 13.8% (93/672) on PutnamBench.
The diffusion prover is a proof of concept (4B only; accuracy gap not fully characterized).

Takeaways

In data-scarce domains, augmentation methods like ALF may beat adding parameters.
Curriculum learning matters for long-sequence, complex-reasoning tasks.
Diffusion is not just for images — any iteratively refinable task (text, code, proofs) may benefit.

Core conclusion: via stratified data, curriculum learning, and ALF augmentation, Pythagoras-Prover's 4B model beats the 671B DeepSeek-Prover-V2 on MiniF2F (86.1% vs 82.4%), its 32B model sets open-source SOTA (93.0%), and its diffusion variant proves 2.58x faster — showing that smart data strategy can outweigh massive scale in formal proving.