Ce professeur de mathématiques butait sur ce problème depuis 5 ans : une IA le résout en une seule nuit

L'IA AxiomProver, créée par la startup Axiom, vient de démontrer quatre conjectures mathématiques majeures. Le cas le plus spectaculaire concerne le professeur Dawei Chen, bloqué pendant cinq ans sur une formule de géométrie ; l'IA a fourni une preuve complète en quelques heures. La clé de sa réussite réside dans la reformulation du problème selon un angle inédit, réduisant la démonstration à une identité mathématique connue.

Les trois autres résultats couvrent des domaines variés : les semi-groupes numériques (algèbre et théorie des nombres), la combinatoire (construction de suites infinies évitant certaines propriétés, avec un écart de 40 000 fois les prévisions probabilistes) et la théorie des nombres (démonstration que la quasi-totalité des nombres premiers satisfait une propriété liée au théorème de Vandiver). Tous les résultats sont vérifiés formellement en Lean, un langage informatique qui permet de vérifier chaque étape mécaniquement, et les démonstrations sont publiées en open-source sur GitHub pour reproduction complète.

Cette percée illustre une nouvelle approche de la validation scientifique : les machines explorent des chemins que l'esprit humain n'avait pas empruntés, ouvrant la voie à un « mathématicien artificiel » capable de naviguer autonomement dans l'espace mathématique.