Le théorème de Fermat expliqué en très simple
Le dernier théorème de Fermat est célèbre parce que son idée est extrêmement simple à comprendre, alors que sa démonstration a résisté pendant plus de trois siècles.
Prenons d’abord des nombres au carré. On peut écrire : 3² + 4² = 5². Cela donne 9 + 16 = 25. Donc, au carré, il existe bien trois nombres entiers qui fonctionnent.
Fermat affirme qu’à partir du cube, puis pour toutes les puissances supérieures, cela devient impossible. Autrement dit, on ne peut trouver aucun trio de nombres entiers positifs a, b et c qui vérifie aⁿ + bⁿ = cⁿ lorsque n est supérieur à 2.
En version encore plus simple : au carré, certaines combinaisons marchent. Au cube, à la puissance 4, 5, 6 et au-delà, Fermat dit qu’aucune combinaison entière ne marchera jamais.
Le vertige vient de là : essayer des milliards de nombres ne suffit pas. Il fallait démontrer que c’est impossible pour une infinité de nombres. Fermat avait écrit vers 1637 qu’il possédait une démonstration merveilleuse, mais qu’elle était trop longue pour tenir dans la marge de son livre. Il ne l’a jamais laissée. Il faudra attendre Andrew Wiles, avec Richard Taylor pour la correction finale, et une publication en 1995 pour obtenir une preuve acceptée.
Onze jours pour transformer une montagne de mathématiques en preuve vérifiable
Selon Anthropic, Tianyi Peng et son équipe voulaient initialement tester jusqu’où Claude pouvait aller dans la formalisation du dernier théorème de Fermat. Le résultat a dépassé leurs attentes : en onze jours, Claude a produit une preuve de bout en bout vérifiée par ordinateur.
Anthropic annonce environ 13 millions de lignes de code Lean. Les agents ont démontré environ 30 300 théorèmes intermédiaires, dont près de 29 500 sont utilisés dans le chemin final de la preuve. Le dépôt public indique que le résultat s’appuie sur Lean 4, Mathlib et l’argument mathématique issu de Frey, Serre, Ribet, Wiles et Taylor-Wiles.
Le chiffre est spectaculaire, mais la vraie nouveauté n’est pas la longueur. C’est le fait que l’ensemble puisse être contrôlé par un assistant de preuve. Lean ne se contente pas de lire un texte et de dire qu’il semble correct. Il vérifie les dépendances logiques et refuse une démonstration si les étapes nécessaires ne sont pas établies.
Il n’a pas résolu Fermat une deuxième fois
Cette nuance est essentielle. Le dernier théorème de Fermat était déjà démontré. Andrew Wiles avait présenté une première preuve en 1993, une faille avait ensuite été découverte, puis Wiles et Richard Taylor avaient trouvé la correction. La preuve complète a été publiée en 1995.
Claude n’a donc pas trouvé une nouvelle solution inconnue de l’humanité. Il a accompli une autre tâche, très difficile : formaliser cette architecture mathématique pour qu’un ordinateur puisse la vérifier automatiquement.
Un texte destiné à des mathématiciens peut sauter des étapes considérées comme évidentes. Une machine exige au contraire que chaque pièce soit explicitée. Anthropic souligne que le projet communautaire de formalisation lancé en 2024 autour de Kevin Buzzard, à Imperial College London, était envisagé comme un travail de plusieurs années.
Des dizaines d’agents ont dû apprendre à collaborer
Le plus intéressant est peut-être la méthode. Anthropic décrit des dizaines d’agents Claude travaillant en parallèle : certains définissaient des concepts, d’autres cherchaient des démonstrations intermédiaires, d’autres encore réutilisaient les résultats déjà obtenus.
Les premières tentatives ont échoué. Les agents perdaient le fil de l’état général du projet et collaboraient mal. L’équipe a alors utilisé Prove2Me, une infrastructure qui représente les théorèmes et leurs dépendances sous forme de graphe. Les agents pouvaient ainsi savoir ce qui était déjà démontré, ce qui restait à faire et quels résultats des autres agents pouvaient être réutilisés.
Avec cette structure, le système a pu progresser vers des sous-problèmes de plus en plus complexes. Anthropic indique que l’intervention humaine mathématique s’est limitée à quelques instructions de haut niveau.
L’IA pourrait devenir le contrôleur qualité des mathématiques produites par l’IA
Kevin Buzzard, qui dirige le projet de formalisation du dernier théorème de Fermat à Imperial College London, a examiné le résultat et l’a qualifié d’extraordinaire. Pour lui, cette réussite marque une étape importante vers la formalisation automatique de la littérature mathématique moderne.
L’enjeu dépasse largement Fermat. Une preuve humaine très longue peut contenir une erreur minuscule qui demande des mois ou des années à être détectée. Si des outils comme Claude et Lean peuvent transformer des démonstrations complexes en objets contrôlables par machine, ils pourraient aider à repérer des erreurs dans des résultats existants et à vérifier plus rapidement les nouvelles mathématiques.
Et il existe un paradoxe intéressant : plus les IA seront capables de produire elles-mêmes des démonstrations, plus il deviendra difficile pour les humains de tout vérifier manuellement. L’IA pourrait donc devenir à la fois productrice de mathématiques et auxiliaire chargé d’en vérifier la cohérence formelle.
La prochaine énigme ne sera pas forcément une formalisation
Le rapprochement avec la conjecture de Syracuse vient naturellement. Là aussi, la règle du jeu est très simple à expliquer et pourtant personne n’a encore réussi à démontrer le résultat général.
La différence est fondamentale : pour Fermat, Claude disposait d’une preuve humaine déjà connue qu’il fallait formaliser. Pour Syracuse, il n’existe toujours pas de démonstration complète connue à traduire dans Lean. Il faudrait donc faire davantage que vérifier : il faudrait découvrir une idée mathématique nouvelle.
C’est précisément là que se trouvera le prochain véritable test. Ces systèmes multi-agents sont-ils seulement capables d’absorber et de formaliser des constructions humaines gigantesques, ou pourront-ils un jour produire l’idée qui manque encore à l’humanité sur un problème ouvert ? À ce stade, personne ne peut l’affirmer.
