Le concours Putnam, le concours de mathématiques universitaires le plus difficile au monde, s'est terminé hier à 16h00, heure du Pacifique. À 15h58, AxiomProver @axiommathai a résolu de manière autonome 8/12 de Putnam2025 en Lean, un langage 100% vérifiable. L'an dernier, notre score nous aurait placés 4e sur environ 4000 et nous aurions obtenu la bourse Putnam (dans le top 10 ces dernières années).
L'examen William Lowell Putnam est le concours universitaire le plus prestigieux au monde. La note médiane est souvent de 0. Axiom est une jeune entreprise de quatre mois basée à Palo Alto. Nous développons le point de départ du raisonnement : un mathématicien IA. Lean est un langage 100% vérifiable par machine.
Voici notre première étape. Il y a quatre mois, nous avions des chaises de camping et des tables en plastique achetées dans une brocante. Les tableaux blancs étaient faits de post-it collés aux murs. Tout le monde était ravi de notre premier canapé. Nous avons désormais établi nos racines de l'autre côté de l'Atlantique. Une équipe de génies des mathématiques et de l'ingénierie, réunie en un seul lieu !
Les personnes à l'origine de notre système AxiomProver sont passionnées par les mathématiques, les langages de programmation et l'IA – les 3 piliers. Ils débattent de la naturalité d'une formalisation. Ils s'enthousiasment lorsqu'une preuve est validée grâce aux techniques de compilation. Ce travail est technique, mais il est aussi profondément humain.
Nous nous tenons sur les épaules de géants – @leanprover, la communauté Mathlib et les chercheurs universitaires et industriels. Merci, et nous développons des outils pour servir la communauté via de futures versions. Nous félicitons les participants du Putnam et célébrerons très prochainement vos succès.
@axiommathai apprécierait vos retweets !