En 2024, l’Olympiade internationale de mathématiques a marqué une étape historique. Alors que le concours est traditionnellement une bataille d’esprit entre les étudiants les plus brillants du monde, un participant non officiel a volé la vedette : AlphaProof de Google DeepMind. Le programme d’IA a obtenu une médaille d’argent, prouvant que les machines ne se contentent plus de calculer des nombres : elles commencent à maîtriser l’art du raisonnement logique.
Cette percée n’est pas un miracle isolé de l’ingénierie ; c’est le résultat d’une évolution de plusieurs décennies dans la façon dont nous vérifions la vérité par le code. Dans son nouveau livre, The Proof in the Code, le journaliste Kevin Hartnett explore le parcours improbable de Lean, un outil logiciel qui est passé d’un assistant de codage de niche à l’épine dorsale de la vérification mathématique et du développement de l’IA modernes.
Le pont entre le code et la logique
L’histoire commence avec Leo de Moura, un ancien ingénieur de Microsoft Research qui a lancé Lean en 2013. Conçu à l’origine comme un outil permettant de vérifier les erreurs dans le code logiciel, le véritable potentiel du Lean résidait dans sa similitude structurelle avec les mathématiques.
Comme le souligne Hartnett, les deux disciplines partagent un ADN fondamental :
– Syntaxe : Les deux nécessitent des instructions précises, étape par étape.
– Logique : Une seule erreur dans une ligne de code est fonctionnellement identique à un « écart » dans une preuve mathématique.
– Exécution : Tout comme un programme ne s’exécute que si la logique est solide, un théorème mathématique n’est valide que si sa preuve est hermétique.
Cette prise de conscience a déclenché un mouvement. Même si Lean ne pouvait pas « inventer » de nouvelles mathématiques à lui seul, il agissait comme un démonstrateur interactif de théorèmes. Il faudrait une preuve écrite par un humain (qui pourrait s’étendre sur des centaines de pages et prendre des mois pour être examinée par des pairs) et vérifier son exactitude absolue en un instant.
La lutte pour un « langage mathématique »
La transition des mathématiques traditionnelles à la preuve numérique ne s’est pas faite sans heurts. Pendant des années, les mathématiciens ont été confrontés à un redoutable problème de « l’œuf et de la poule » : pour rendre le Lean utile, ils avaient besoin de vastes bibliothèques de définitions mathématiques codées ; mais pour construire ces bibliothèques, ils avaient besoin de mathématiciens pour utiliser le programme.
La friction était souvent absurdement granulaire. Hartnett décrit comment le professeur Kevin Buzzard de l’Imperial College de Londres, alors qu’il enseignait aux étudiants de premier cycle, s’est retrouvé coincé parce que Lean lui a demandé de prouver que 2 n’est pas égal à 1. Pour un humain, c’est une vérité évidente ; pour un système logique formel, il s’agit d’un fait fondamental qui doit être explicitement défini avant que tout raisonnement ultérieur puisse avoir lieu.
Surmonter ces obstacles a nécessité des efforts massifs et collaboratifs :
* Numérisation massive : en 2018, les mathématiciens ont passé des mois à traduire des concepts complexes tels que les « espaces perfectoïdes » en milliers de lignes de code.
* Création de communauté : Un petit groupe de chercheurs dévoués a travaillé pour rendre le logiciel convivial, le faisant passer d’un outil académique encombrant à une plate-forme robuste.
* Mise à l’échelle : En 2025, l’écosystème avait explosé, avec des dizaines de milliers d’utilisateurs du monde universitaire et de l’industrie technologique contribuant aux bibliothèques Lean.
Pourquoi c’est important : la quête d’une “machine à vérité”
La convergence des mathématiques et de l’IA est le but ultime de ce mouvement. Pour les ingénieurs logiciels comme de Moura, le prix était une « machine à vérité » qui pouvait garantir qu’un logiciel comme Microsoft Word était totalement exempt de bogues. Pour les mathématiciens, c’est un moyen de garantir que même les découvertes abstraites les plus complexes sont irréprochables.
Pour les chercheurs en IA, le Lean constitue le terrain de formation ultime. En fournissant une bibliothèque massive et vérifiée de vérités mathématiques, Lean permet à des modèles comme AlphaProof d’apprendre un raisonnement rigoureux plutôt que la simple reconnaissance de formes. Ceci est essentiel pour résoudre le problème des « hallucinations » dans l’IA – la tendance des modèles à énoncer de fausses informations avec confiance. Si une IA peut être entraînée à suivre les lois strictes et inflexibles de la logique mathématique, elle pourrait éventuellement appliquer la même rigueur au raisonnement du monde réel.
“Les mathématiques et le codage sont écrits dans une syntaxe exacte sous la forme d’une série d’étapes logiques, chacune menant à la suivante.”
Conclusion
The Proof in the Code raconte comment un outil spécialisé pour le débogage de logiciels est devenu le fondement d’une nouvelle ère de certitude mathématique et d’intelligence artificielle. Il met en évidence un changement profond dans la science : le mouvement vers un avenir où l’intuition humaine et la vérification numérique travailleront en tandem pour définir ce qui est vrai.
