Verifier-guided training, not parameter count, is deciding who wins at Lean 4 theorem proving.
A 4B-parameter model now beats a 671B giant on Lean theorem proving. Pythagoras-Prover (≈4B parameters) achieves 86.1% pass@32 on MiniF2F-test. DeepSeek-Prover-V2-671B gets 82.4% on the same benchmark using roughly 167× more parameters—and loses (arXiv, "Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation," 2026).
That's not the interesting part. The interesting part is why—and what the coverage gets wrong when it stops at the headline.
Here's the short version: the 4B model didn't win because small models are inherently smarter per parameter. It won because its training pipeline was better designed for this task. Understanding that distinction is what determines whether this result matters for your use case.
TL;DR
- Pythagoras-Prover (≈4B) hits 86.1% pass@32 on MiniF2F vs 82.4% for DeepSeek-Prover-V2-671B—using 167× fewer parameters (arXiv, "Pythagoras-Prover," 2026)
- Goedel-Prover-V2-8B achieves 84.6% pass@32, outperforming the 671B baseline despite being 80× smaller; the 32B variant reaches 90.4% in self-correction mode (arXiv, "Goedel-Prover-V2," 2025)
- The wins come from verifier-guided self-correction, scaffolded curriculum data, and model averaging—not from any special property of small models; the same recipe applied to a larger backbone would likely do even better
- No published paper has measured cost-per-proof under identical agentic scaffolds—the comparison isn't compute-fair, and practitioners cannot assume the 4B model is cheaper end-to-end
- On broader Lean tasks, a 70B general model still outperforms math-specific smaller models (NLP4Science, "Benchmarking Automated Theorem Proving with Large Language Models," 2024)
- Choose training-recipe alignment with your proof domain, not model size
The 4B vs 671B Claim: What the Numbers Actually Say
The benchmarks are real, and they're striking.
Goedel-Prover-V2-8B achieves 84.6% pass@32 on MiniF2F, outperforming DeepSeek-Prover-V2-671B's 82.4% under the same metric—despite being 80× smaller (arXiv, "Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction," 2025). The 32B variant advances further: 88.1% in standard mode and 90.4% in self-correction mode (same source). Pythagoras-Prover pushes the DeepSeek-671B baseline from 82.4% to 86.1% pass@32 using 167× fewer parameters (arXiv, "Pythagoras-Prover," 2026).
OProver-32B goes furthest, hitting 93.3% on MiniF2F—outperforming DeepSeek-Prover-V2-671B across all five benchmark evaluations in their comparison (36Kr Europe, "32B Outperforms 671B: OProver, Fully Open-Source Math Theorem-Proving Model," 2025).
On PutnamBench (college-level math), the contrast is even sharper: Goedel-Prover-V2-32B solves 86 problems at pass@184. DeepSeek-Prover-V2-671B solves 47 at pass@1024—fewer problems with almost six times the sampling budget (arXiv, "Goedel-Prover-V2," 2025).
What pass@32 means: you sample 32 proof attempts per theorem; the problem counts as solved if any attempt succeeds. It's the standard reproducible metric for Lean 4 theorem proving, which is why these comparisons hold up.
The Lean 4 compiler is the ground truth. No partial credit, no plausible-but-wrong. Either the proof compiles or it doesn't.
The headline numbers check out. But they're measuring something more specific than "parameter count determines performance."
Why This Isn't Just "Parameter Efficiency"
The win isn't magic. It's a pipeline.
Goedel-Prover-V2's advantage comes from three mechanisms working together (arXiv, "Goedel-Prover-V2," 2025):
1. Scaffolded data synthesis. The training curriculum generates progressively harder synthetic proof tasks. Instead of random theorem exposure, the model masters intermediate steps before tackling complex proofs. Difficulty ramps as competence grows.
2. Verifier-guided self-correction. After generating a proof attempt, the Lean compiler reports exactly where it failed. The model revises based on that specific error. This tight loop—generate, compile, error message, revise—is fundamentally different from black-box sampling, where you generate 32 candidates and hope one works.
3. Model averaging. Checkpoint merging across training stages preserves output diversity. Late-stage RL tends to collapse outputs toward a narrow distribution; averaging multiple checkpoints keeps the proof search exploratory.
DeepSeek-Prover-V2-671B trained on 8 million synthetic formal statements—a massive corpus (arXiv, "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning," 2025). But that training didn't include the tight verifier loop Goedel-Prover-V2 uses. The 671B model generates proof candidates; it doesn't iteratively repair them using compiler feedback.
The key insight the paper itself makes: Goedel-Prover-V2 does not claim that 8B models are inherently more parameter-efficient than 671B models. The paper reports "clear performance scaling with model size" when their training pipeline is applied (University of Virginia, "Major Breakthroughs in Lean 4-Based Auto-Formalized Mathematics," 2025). A 671B model trained with the same recipe would likely outperform both. The 4B/8B win is a win for the training recipe, not for smallness.
Generate, compile, fail, revise. The verifier loop is what separates these models from black-box sampling.
The Compute-Parity Problem Nobody Is Measuring
Here's what the papers don't answer: if you gave both models the exact same compute budget—same proof-attempt count, same context length, same Lean tactic limits—who wins?
Every current comparison is structurally unfair. Goedel-Prover-V2 uses verifier-guided self-correction loops; DeepSeek-Prover-V2-671B's baseline evaluation doesn't. Pythagoras-Prover was designed around efficient Lean augmentation; the 671B baseline was trained with a different objective and tested differently. They weren't measured under identical conditions.
QED-Nano (4B) illustrates exactly how much scaffolding moves the needle. Without any agentic scaffold, QED-Nano achieves 40% on IMO-ProofBench. Add a Reasoning-Scaffold Agent allowing up to 2M tokens per problem, and it reaches 57% (arXiv, "QED-Nano: Tiny LLM Proves Olympiad Theorems," arXiv:2604.04898, 2026). That's a 43% relative improvement from compute budget alone. Now ask: what would a frontier model achieve on the same benchmark with the same 2M-token budget? The paper doesn't test this.
OpenAI's o4-mini demonstrates the global-planning problem from a different angle: it achieves 98.88% accuracy at individual reasoning steps but fails to assemble full proofs (OpenReview, "Scalable Synthesis of Theorem Proving Challenges in Frontier LRMs," 2026). Local reasoning competence doesn't guarantee global proof construction. The small models with verifier loops bypass this gap not through superior reasoning—they bypass it through better search and repair.
The missing measurement isn't a gotcha. It's the real engineering question: proof-per-dollar under matched scaffolds. Until someone publishes it, "4B is cheaper" is an inference from parameter count, not a measured fact.
Where Small Models Still Lose
On a shared evaluation framework, a general-purpose LLaMa-70B model still outperforms math-specific smaller models at Lean theorem proving (NLP4Science, "Benchmarking Automated Theorem Proving with Large Language Models," 2024). The finding is direct: "a general-purpose large model like LLaMa-70B still has edge over math-specific smaller models for the task under consideration." Same proving framework, same task distribution—bigger still wins there.
Domain brittleness hits everyone. DeepSeek-Prover-V2-671B reaches 57.5% on Busy Beaver problems but only 12% on Mixed Boolean Arithmetic, revealing that even a 671B specialist can collapse on out-of-distribution proof families (OpenReview, "Scalable Synthesis of Theorem Proving Challenges in Frontier LRMs," 2026). OpenAI o3 and o4-mini can't break 35% on the BB challenge (same source). Nobody handles hard OOD proof domains reliably, large or small.
Scaling laws for proof tasks still trend positive with model size when training paradigms are held constant. Research on proof artifact co-training finds that "performance is highly correlated with model size, with larger models generally achieving better generalization even in the overfitted regime" (cited in arXiv, "Goedel-Prover-V2," 2025). Remove the training-pipeline advantage and smaller models don't automatically win.
Daniel Litt, an algebraic geometer tracking LLMs against real research-level mathematics, summarized the practical ceiling: "As far as I know no team outside a big lab significantly outperformed GPT 5.2 Pro 'out-of-the-box,' even with somewhat involved scaffolds" (public commentary, 2025). On non-benchmark math—problems with no known answer key—frontier general models still set the bar.
The "small beats giant" result is real on MiniF2F. It doesn't transfer universally.
What This Means for Your Verification Agent
Model choice for theorem proving isn't about size—it's about task alignment. Here's a five-point evaluation before you commit:
1. Match your proof domain first. MiniF2F covers high-school and Olympiad Lean theorems. If your proofs look like that—formal software verification, Lean-based correctness proofs for data structures—Goedel-Prover-V2 or Pythagoras-Prover likely beats a general frontier model. For abstract algebra, topology, or novel domains, frontier models still lead.
2. Measure cost-per-proof on your benchmarks. Don't trust MiniF2F transfer. Pick 50 representative problems from your actual domain. Run both a specialized 4B/8B model and a frontier model. Measure GPU-seconds and total inference cost per solved theorem. The ratio may surprise you in either direction.
3. Budget for the verifier loop's latency. Verifier-guided self-correction adds compile-cycle overhead. Each revision triggers a Lean compiler call. Measure time-to-first-valid-proof, not just pass@k. A 4B model that passes at pass@8 with three revision cycles may be slower end-to-end than a larger model passing at pass@1.
4. Account for retraining costs. Off-the-shelf Goedel-Prover-V2 and Pythagoras-Prover were trained on Lean MiniF2F-style data. If your domain differs, domain-specific fine-tuning is part of the total cost. It's rarely included in "4B is cheaper" arguments.
5. Compare full-pipeline cost, not model cost alone. Token cost for the base model is a fraction of the real bill. Scaffold latency, Lean compiler calls, retry loops, and amortized retraining compute give you actual cost-per-proof. That number is what matters.
Teams using Mesh API's compare endpoint can route the same prompts to multiple models simultaneously—including open specialized models alongside frontier APIs—and get real latency and cost data on your actual workload before committing to an architecture.
The Real Reason: Training Data Beats Parameters
Every piece of evidence points the same direction.
Goedel-Prover-V2 uses expert iteration, RL on Lean compiler feedback, scaffolded curriculum, and model averaging. QED-Nano uses SFT followed by rubric-shaped RL designed to generate high-quality proofs. OProver uses M-A-P architecture with internalized retrieval and multi-round proof repair. Each approach builds a tight verifier integration rather than relying on scale to compensate for a loose training signal.
DeepSeek-Prover-V2-671B trained on 8 million synthetic formal statements (arXiv, "DeepSeek-Prover-V2," 2025)—a massive corpus—but without the tight verifier loop that enables iterative self-correction. The 671B model is strong. It's just under-aligned with the specific task of Lean theorem proving via repair.
The obvious next step that nobody has published: apply Goedel-Prover-V2's training recipe to a 671B backbone. The paper's own observation—"clear performance scaling with model size" when their pipeline is used—implies this would produce better results than any current system. It's almost certainly being attempted.
"Sample efficiency" (fewer training examples to reach a threshold) is not the same as "parameter efficiency" (fewer parameters to reach a threshold). The small-model wins here are about the former. No published evidence supports the latter.
The broader picture: nobody has solved theorem proving. Small models win on specific benchmarks with specific training pipelines. Apply the same recipe to a larger backbone, and the "small" advantage likely disappears. We're watching a training-pipeline competition that happens to correlate with model size. The pipeline is doing the work.
FAQ
Can I use a 4B theorem-proving model in production?
Yes, with caveats. If your domain overlaps with Lean 4 MiniF2F or Olympiad-style proofs, Goedel-Prover-V2 or Pythagoras-Prover likely outperforms a general frontier model on that specific task. For broad mathematical coverage—topology, category theory, novel domains—frontier models still lead. Always benchmark on your actual problems first.
How much does inference cost compare between 4B and 671B models for theorem proving?
No paper has published cost-per-proof under identical agentic setups. Raw model inference is cheaper at 4B, but that ignores verifier loop calls, Lean compiler overhead, scaffold tokens, and revision cycles. Actual cost-per-solved-theorem may differ significantly from naive parameter-count scaling. Measure it on your workload.
Will Pythagoras-Prover or Goedel-Prover-V2 work on my proof domain?
Only if your proofs are structurally similar to Lean 4 MiniF2F or Olympiad-style mathematics. For software verification, cryptographic properties, or abstract algebraic structures, you'll likely need domain-specific fine-tuning or scaffolds. Generalization outside the MiniF2F distribution is still an open research question.
What's the real catch with "4B beats 671B"?
The win requires three simultaneous conditions: the right benchmark (MiniF2F, PutnamBench), the right training (verifier-guided RL, synthetic curriculum), and the right scaffolding (tight Lean compiler loop). Remove any of those three and the win may not hold. On broader tasks and OOD problems, larger models still dominate.
If small models win through better training, why doesn't everyone use them?
Replicating Goedel-Prover-V2's pipeline requires Lean expertise, synthetic proof generation infrastructure, and RL-tuning compute. For most teams, a frontier model API call is faster to ship than a specialized fine-tuning run. The small-model win is real for teams with Lean-specific workloads—it's not a general signal to avoid large models.