Preuves mathématiques OpenAI en Lean : vérifiables sur GitHub
OpenAI a déposé 722 manuscrits mathématiques sur GitHub, formalisés en Lean et vérifiables par ordinateur. Ces preuves sortent d’un modèle interne et incluent des résultats majeurs comme une solution aux équations de Navier-Stokes. Le dépôt openai/math est accessible sous licence Apache 2.0.