Goedel-Prover

Chi Jin's open-source Lean 4 theorem-proving line, the SOTA open prover at each release. Goedel-Prover (Feb 2025) reached 57.6% on miniF2F; Goedel-Prover-V2 (Aug 2025) hit 90.4% miniF2F at 32B in self-correction mode — beating DeepSeek-Prover-V2-671B — with an 8B matching 671B-class performance, plus a Goedel-Formalizer-V2; and Goedel-Code-Prover-8B (Mar 2026) applies hierarchical proof search to Lean 4 code verification (62.0% vs 21.8% for DeepSeek-Prover-V2-671B on Verina/Clever/AlgoVeri). Princeton-led, with heavy NVIDIA/Meta/Tsinghua/Stanford collaboration on V2. Models are post-trained from open bases, not pretrained from scratch.