Goedel-Proverは、自動定理証明に特化したオープンソースの大規模言語モデルです。自然言語の数学問題を形式言語（Lean 4など）に変換し、形式化された証明を生成することで、数学問題の自動証明効率を大幅に向上させます。miniF2Fベンチマークテストでは57.6％の成功率を達成し、他のオープンソースモデルを凌駕しています。主な利点としては、高性能、オープンソースによる拡張性、および数学問題に対する深い理解力などが挙げられます。Goedel-Proverは、自動定理証明技術の発展を促進し、数学研究や教育に強力なツールを提供することを目指しています。