Primary evidence
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionS1 · Primary research · Paper · 2025-08-05
- Goedel-Prover-V2 model and theorem-proving repositoryS1 · Primary research · Repository
Goedel-Prover-V2 scales open theorem proving with self-correction
The system uses scaffolded data synthesis, verifier-guided iterative repair and model averaging.
What happened?
Goedel-Prover-V2-32B reported 90.4% miniF2F in self-correction mode and 86 solved PutnamBench problems under its reported evaluation.
Why it matters
It strengthened the case for compact open provers that spend computation on correction rather than only increasing parameter count.
Significance rationale: Goedel-Prover-V2 showed that scaffolded synthetic data and Lean-guided self-correction could deliver strong open theorem-proving performance with much smaller models.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic
- AI contribution
- The model generates Lean proofs and iteratively repairs them using compiler feedback.
- Human contribution
- Researchers designed staged synthesis, self-correction and model-merging procedures.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- goedel-prover-v2, lean
- Organizations
- princeton-university, nvidia
- Problems
- minif2f, putnambench
- Methods
- self-correction, synthetic-data, formal-proof
Sources & artifacts
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionS1 · Primary research · Paper · accessed 2026-09-10
- Goedel-Prover-V2 model and theorem-proving repositoryS1 · Primary research · Repository · accessed 2026-09-11
- Goedel-Prover-V2 model and evaluation artifactsArtifact · Code
Verification history
- 2025-08-05 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.