On the 488-problem miniF2F benchmark for formal mathematics, Stanford researchers found that an AI prover fine-tuned to write Lean 4 proofs solved more problems than a general-purpose model four times its size. In the paper’s no-context setting, the smaller Goedel-Prover-V2-8B solved 205 problems (42.0%), while general-purpose Qwen3-32B solved 62 (12.7%). Lean 4 is a proof assistant that checks whether each proof follows formal rules.
The study asks whether structured mathematical context helps more than training a model for formal proof. The team built MathKG, a graph of 364 theorems and definitions from the Mathlib library, linked by 9,434 typed relations such as “generalizes” and “analogous to.” Five models were tested with graph context, Mathlib retrieval, both, or neither. Results are pass@32: each prover could make up to 32 attempts, using Lean’s error messages to refine failed proofs.
Fine-tuning produced the largest consistent change. On miniF2F, the Lean-specialized Goedel-Prover-V2 gained about 35 percentage points over its Qwen3 base at 8B and 36 points at 32B. By contrast, no single context-augmentation mode improved any model’s total solve rate by more than three points.
Extra context was not uniformly useful. Compared with the same model using no added context, the knowledge graph helped Goedel-Prover-V2-8B solve 14 more miniF2F problems but left general Qwen3-32B with 14 fewer. Mathlib retrieval did not raise aggregate solve rates. The modes also solved different problems. In a matched-budget analysis, the paper combined the problems solved by all four modes, each given eight attempts; that union found 27 more problems for Goedel-Prover-V2-8B than its no-context run with 32 attempts. This is a retrospective comparison, not a tested selector that chooses a mode before solving.
The result points to context selection as a possible complement to specialization, not a replacement for it. The graph covers a curated 364-node core drawn from a library with more than 285,000 verified theorems, and the paper’s open-ended discovery mode was not evaluated. Its evidence therefore concerns specific formal-proof benchmarks, rather than general mathematical reasoning or autonomous discovery.
Sources
- Stanford researchers’ paper, “When Does Structured Knowledge Help Neural Theorem Proving?”.
- Authors’ MathAgent code and evaluation repository.
- Illustrative blackboard photograph by Vitaly Gariev, Unsplash; free under the Unsplash License and not part of the study.