Skip to content
← Models
Open weightsPrinceton University researchers (Yong Lin et al.)/10 trustVerified

Goedel-Prover-SFT

Open-source Lean 4 whole-proof generation via a verifier-in-the-loop data flywheel — 57.6% on miniF2F, #1 on PutnamBench at release.

Visit official page →

About

Goedel-Prover attacks the core bottleneck in formal theorem proving: there just aren't enough Lean proofs to train on. The team's answer is a data flywheel — autoformalize 1.64 million competition math statements from natural language into Lean 4, prove what you can with the current model, keep only the Lean-verified proofs, and retrain. Eight rounds of this expert iteration produced the SFT model.

The payoff was a new open-source state of the art: 57.6% pass@32 on miniF2F, 7.6 points clear of DeepSeek-Prover-V1.5-RL, plus 7 solved PutnamBench problems for the #1 leaderboard spot and nearly 30K new Lean Workbook proofs. The follow-up V2 line later pushed past 88%, but the SFT release remains the clean, reproducible baseline. Everything is MIT-licensed on GitHub and Hugging Face.

Specs

Context window

Not officially published (DeepSeek-Prover-V1.5-Base foundation)

Pricing

Free / open weights

Free quota

Fully open — no API

API access

No official API — self-host from Hugging Face (Goedel-LM/Goedel-Prover-SFT)

Weights

Open weights

Released

Not disclosed

Benchmarks

  • Paper-reported (arXiv 2502.07640): 57.6% Pass@32 on miniF2F, +7.6pp over DeepSeek-Prover-V1.5-RL
  • Same paper: 7 PutnamBench problems solved @Pass@512 (#1 on the leaderboard); 29.7K Lean Workbook proofs generated

Provider-reported unless a source says otherwise. Benchmarks are marketing-adjacent by nature — treat them as directional.

Use cases

theorem-provingformal-verificationlean4math-research

Trust score — 8/10

/10 trustVerified

Scored 8/10 (TIER verified, metrics-v1). Evidence: peer-style paper (arXiv 2502.07640) from Princeton researchers with miniF2F and PutnamBench results; MIT license confirmed via HF API; open code, weights and datasets (Goedel-LM org); widely cited in the ATP community. Strengths: transparent data flywheel methodology, permissive license, reproducible. Docked for: (1) headline numbers are author-reported; (2) whole-proof generation only — no tactic-level search. License: MIT.

How the trust score is built

Full methodology →
Adoption · stars/downloads, log-scaled vs peers
7.0/10
Maintenance · recency, releases, issue load
7.0/10
Openness · license + docs
9.0/10
Manual review · sanity read + red-flag check
8.0/10
  • · Princeton researchers; released 2025-02-11
  • · Paper arXiv 2502.07640; 57.6% Pass@32 miniF2F, #1 PutnamBench
  • · Benchmarks are author-reported

Sources