Goedel-Prover est un grand modèle linguistique open source spécialisé dans la preuve de théorème automatisée. Il améliore considérablement l'efficacité de la preuve automatisée des problèmes mathématiques en traduisant les problèmes mathématiques en langage naturel dans un langage formel (comme Lean 4) et en générant des preuves formelles. Ce modèle a atteint un taux de réussite de 57,6 % lors du test de référence miniF2F, surpassant d'autres modèles open source. Ses principaux avantages incluent des performances élevées, une extensibilité open source et une compréhension approfondie des problèmes mathématiques. Goedel-Prover vise à faire progresser les techniques de preuve de théorème automatisée et à fournir un support puissant aux outils pour la recherche et l'enseignement des mathématiques.