title: Goedel-Prover: A Frontier Model for Open-Source Automated Theorem
    Proving
summary: We introduce Goedel-Prover, an open-source large language model (LLM) that
  achieves the state-of-the-art (SOTA) performance in automated formal proof
  generation for mathematical problems. The key challenge in this field is the
  scarcity of formalized math statements and proofs, which we tackle in the
  following ways. We train statement formalizers to translate the natural
  language math problems from Numina into formal language (Lean 4), creating a
  dataset of 1.64 million formal statements. LLMs are used to check that the
  formal statements accurately preserve the content of the original natural
  language problems. We then iteratively build a large dataset of formal proofs
  by training a series of provers. Each prover succeeds in proving many
  statements that the previous ones could not, and these new proofs are added to
  the training set for the next prover. The final prover outperforms all existing
  open-source models in whole-proof generation. On the miniF2F benchmark, it
  achieves a 57.6% success rate (Pass@32), exceeding the previous best
  open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7
  problems (Pass@512), ranking first on the leaderboard. Furthermore, it
  generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the
  15.7K produced by earlier works.
paper_authors._id: 67acb6af4335fbde70348fc1
paper_authors.name: Yong Lin
paper_authors._id: 67acb6af4335fbde70348fc2
paper_authors.name: Shange Tang
paper_authors._id: 67acb6af4335fbde70348fc3
paper_authors.name: Bohan Lyu
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2025-02-18T09:34:20.642Z
paper_authors._id: 650267e7e751d03da933a24a
paper_authors.avatarUrl: /avatars/f047a047d1de304cd97027463541bdf3.svg
paper_authors.fullname: Bohan22
paper_authors.type: user
paper_authors.user: Bohan22
paper_authors._id: 67acb6af4335fbde70348fc4
paper_authors.name: Jiayun Wu
paper_authors._id: 67acb6af4335fbde70348fc5
paper_authors.name: Hongzhou Lin
paper_authors._id: 67acb6af4335fbde70348fc6
paper_authors.name: Kaiyu Yang
paper_authors._id: 67acb6af4335fbde70348fc7
paper_authors.name: Jia Li
paper_authors._id: 67acb6af4335fbde70348fc8
paper_authors.name: Mengzhou Xia
paper_authors._id: 67acb6af4335fbde70348fc9
paper_authors.name: Danqi Chen
paper_authors._id: 67acb6af4335fbde70348fca
paper_authors.name: Sanjeev Arora
paper_authors._id: 67acb6af4335fbde70348fcb
paper_authors.name: Chi Jin
paper_title: Goedel-Prover: A Frontier Model for Open-Source Automated Theorem
    Proving
paper_summary: We introduce Goedel-Prover, an open-source large language model (LLM) that
  achieves the state-of-the-art (SOTA) performance in automated formal proof
  generation for mathematical problems. The key challenge in this field is the
  scarcity of formalized math statements and proofs, which we tackle in the
  following ways. We train statement formalizers to translate the natural
  language math problems from Numina into formal language (Lean 4), creating a
  dataset of 1.64 million formal statements. LLMs are used to check that the
  formal statements accurately preserve the content of the original natural
  language problems. We then iteratively build a large dataset of formal proofs
  by training a series of provers. Each prover succeeds in proving many
  statements that the previous ones could not, and these new proofs are added to
  the training set for the next prover. The final prover outperforms all existing
  open-source models in whole-proof generation. On the miniF2F benchmark, it
  achieves a 57.6% success rate (Pass@32), exceeding the previous best
  open-source model by 7.6%. On PutnamBench, Goedel-Prover successfully solves 7
  problems (Pass@512), ranking first on the leaderboard. Furthermore, it
  generates 29.7K formal proofs for Lean Workbook problems, nearly doubling the
  15.7K produced by earlier works.
paper_ai_keywords: Goedel-Prover large language model (LLM) automated formal proof generation formalized math statements formal language (Lean 4) statement formalizers natural language math problems formal proofs provers whole-proof generation miniF2F benchmark PutnamBench Lean Workbook problems