Goedel-Prover is an open-source large language model specializing in automated theorem proving. It significantly enhances the efficiency of automated mathematical problem solving by translating natural language mathematical questions into formal languages (such as Lean 4) and generating formal proofs. The model achieved a success rate of 57.6% on the miniF2F benchmark, surpassing other open-source models. Its key advantages include high performance, open-source extensibility, and a deep understanding of mathematical problems. Goedel-Prover aims to advance automated theorem proving technologies and provide powerful tool support for mathematical research and education.