Axiom résout quatre conjectures mathématiques avec l’IA formelle

Une startup IA a résolu quatre conjectures mathématiques en décennies via AxiomProver, un système générant des preuves formelles vérifiées en Lean. Étape majeure en démonstration formelle et collaboration IA-mathématique.

Une collaboration historique : Chen rencontre Ono

Dawei Chen, mathématicien, travaille depuis cinq ans sur un problème de géométrie algébrique avec Quentin Gendron. Leur recherche bute sur un obstacle : une formule de théorie des nombres qu’ils ne parviennent pas à justifier. Ils rédigent un article présentant l’impasse comme une conjecture.

Lors d’une conférence mathématique à Washington, Chen expose le problème à Ken Ono, mathématicien spécialiste de théorie des nombres. Le lendemain matin, Ono lui présente une solution — générée par AxiomProver, le système d’IA développé par Axiom, sa nouvelle entreprise.

Cette rencontre résume bien l’approche : l’IA ne résout pas seule des questions mystérieuses, elle assiste des chercheurs en formalisant et validant des intuitions mathématiques qui restaient bloquées.

Les quatre conjectures résolues (février 2026)

Axiom a annoncé ses résultats le 3 février 2026 via arXiv. Chaque preuve a été entièrement formalisée en Lean, un langage de programmation mathématique où chaque étape logique peut être vérifiée par machine.

1. La conjecture Chen-Gendron

Porte sur les k-différentielles, des objets mathématiques complexes sur les surfaces de Riemann. La preuve repose sur une reformulation en termes de symboles de Jacobi, ramenant le problème à une identité combinatoire et à des résultats classiques du XIXe siècle. Elle a été entièrement formalisée en Lean.

2. La conjecture de Fel

Concerne les syzygies — des relations algébriques complexes entre polynômes. Cette conjecture s’appuie sur des formules découvertes par Srinivasa Ramanujan il y a plus de cent ans, notées dans ses carnets et restées sans connexion évidente jusqu’à présent.

AxiomProver n’a pas simplement comblé un maillon manquant : il a construit la démonstration de zéro, à partir du seul énoncé en langage naturel de la conjecture. Scott Kominers, professeur à Harvard Business School et connaisseur du problème, qualifie le résultat d’« astounding ». « C’est remarquable non seulement que AxiomProver ait pu résoudre ce problème automatisé et instantanément vérifié, mais aussi pour l’élégance mathématique produite. »

3 et 4. Deux conjectures en théorie des nombres

Les détails techniques n’ont pas encore été précisés publiquement, mais suivent le même protocole : génération automatique, formalisation Lean, publication sur arXiv pour examen par les pairs.

Comment fonctionne AxiomProver

AxiomProver combine deux éléments clés : un grand modèle de langage capable de raisonner sur des énoncés mathématiques, et un système de vérification formelle en Lean qui garantit que chaque étape de preuve est logiquement correcte.

Le système opère selon deux modes : collaboratif, où l’IA affine les intuitions d’un chercheur humain, et autonome, où il reçoit un énoncé en langage naturel et construit une démonstration complète sans intervention externe. « C’est un nouveau paradigme pour la démonstration de théorèmes », déclare Ken Ono.

Axiom : une startup à forte densité d'expertise

Fondatrice et leadership

Carina Hong, 24 ans, a cofondé Axiom en mars 2025 en quittant son doctorat à Stanford. Rhodes Scholar, elle s’est entourée de chercheurs issus des plus grands laboratoires IA.

Équipe

• Shubho Sengupta (CTO)
• François Charton, Aram Markosyan, Hugh Leather (anciennement Meta Fundamental AI Research)
• Ken Ono, professeur titulaire à l’Université de Virginie
• Autres recrutements issus de Google Brain et DeepMind

À seulement 17 employés, Axiom concentre une densité exceptionnelle d’expertise en IA théorique et démonstration formelle.

Financement

• 64 millions de dollars levés en septembre 2025
• Menés par B Capital, avec participation de Greycroft, Madrona Venture Group et Menlo Ventures
• Valorisation : environ 300 millions de dollars

Contexte : après AlphaProof de Google DeepMind

En 2024, Google DeepMind avait démontré une approche similaire avec AlphaProof, un système entraîné par apprentissage par renforcement sur des millions de problèmes formalisés. AlphaProof avait atteint le niveau de médaille d’argent aux Olympiades mathématiques internationales (IMO 2024), résolvant trois des six problèmes de compétition.

Les deux systèmes différent sur plusieurs points. AlphaProof cible les problèmes d’olympiade à temps limité ; AxiomProver vise des conjectures de recherche ouverte sans contrainte temporelle. AlphaProof repose sur l’apprentissage par renforcement, tandis qu’AxiomProver combine un LLM et la vérification Lean. Axiom affirme intégrer des avancées techniques significatives, notamment une meilleure capacité à explorer l’espace des preuves et à utiliser Lean efficacement, mais aucune comparaison directe formelle n’a été réalisée entre les deux systèmes.

La perspective des mathématiciens : cautèle et opportunité

Dawei Chen ne voit pas l’IA comme une menace, mais comme un outil complémentaire. « Les mathématiciens n’ont pas oublié les tables de multiplication après l’invention de la calculatrice », rappelle-t-il. Sa vision : « Je crois que l’IA servira d’outil intelligent novateur — ou peut-être est-il plus juste de dire un ‘partenaire intelligent’ — ouvrant des horizons plus riches pour la recherche mathématique. »

Cette posture prudente reflète la réalité : les preuves formalisées en Lean sont vérifiables automatiquement, mais leur acceptation académique définitive dépend de l’examen par les pairs.

Validité académique et applications envisagées

Statut actuel

Les quatre preuves figurent sur arXiv et sont actuellement examinées par les pairs en vue d’une publication dans des revues académiques.

Carina Hong envisage des débouchés au-delà des mathématiques pures : cryptographie, vérification de hardware, finance quantitative. Dans tous ces domaines, les preuves de correction et de sécurité sont critiques. Cependant, aucune mise en production ni client pilote n’a encore été annoncé. L’acceptation définitive par la communauté mathématique reste l’étape décisive pour transformer ces résultats en contributions établies et ouvrir des perspectives commerciales.

FAQ

Qu'est-ce qu'AxiomProver et comment fonctionne-t-il ?

AxiomProver combine un grand modèle de langage avec un système de vérification formelle en Lean, permettant la génération et la validation automatique de preuves mathématiques.

Quelles sont les quatre conjectures résolues par Axiom ?

La conjecture Chen-Gendron (géométrie algébrique), la conjecture de Fel (syzygies polynomiales), et deux problèmes additionnels en théorie des nombres, tous formalisés en Lean et publiés sur arXiv.

Quelle est la différence entre AxiomProver et AlphaProof de Google DeepMind ?

AlphaProof cible les problèmes d’olympiade à temps limité ; AxiomProver vise des conjectures de recherche ouverte sans contrainte temporelle, avec des capacités distinctes d’exploration et d’utilisation de Lean.

Ces preuves sont-elles reconnues par la communauté mathématique ?

Les quatre preuves sont en cours d’examen par les pairs sur arXiv en vue d’une publication académique ; l’acceptation définitive par la communauté reste l’étape décisive.