13 millions de lignes de code en 11 jours : Claude formule le grand théorème de Fermat

La société "Anthropic" a annoncé que le modèle d'intelligence artificielle "Claude" a pu, de manière quasi autonome, formuler le grand théorème de Fermat sous forme de code informatique en seulement 11 jours.

Cela a donné lieu à environ 13 millions de lignes de code dans le langage "Lean", ainsi qu'à environ 29 500 théorèmes intermédiaires, ce qui équivaut à environ cinq fois le volume de la bibliothèque officielle de mathématiques "Mathlib" dans son ensemble.

Il convient de rappeler que le mathématicien français Pierre de Fermat a énoncé ce théorème au XVIIe siècle, mais sa preuve est restée inaccessible pendant plus de trois siècles, jusqu'à ce que le mathématicien britannique Andrew Wiles parvienne à la démontrer en 1995, après environ sept ans de travail en secret.

La formulation formelle signifie traduire la preuve mathématique en code informatique permettant à l'ordinateur de vérifier la validité de chaque étape.

De nombreux mathématiciens ont tenté de trouver une preuve pour ce problème, mais leurs tentatives se sont soldées par un échec. Wiles a travaillé sur cette question en secret pendant sept ans avant d'annoncer en 1993 avoir obtenu une percée majeure. Les preuves mathématiques sont généralement composées de longues chaînes d'arguments logiques qui s'appuient les uns sur les autres, de sorte qu'une erreur dans une étape peut entraîner l'effondrement de toute la preuve.

C'est exactement ce qui s'est produit avec Wiles, lorsqu'une faille a été découverte dans sa preuve, nécessitant près d'un an pour la combler.

La numérisation ou formalisation des théories mathématiques consiste à les transférer du monde du papier et du crayon vers celui du code informatique, permettant aux ordinateurs de les traiter et de vérifier leur logique étape par étape, détectant ainsi toute erreur ou faille. Le dépôt central "Mathlib" contient environ deux millions de lignes de mathématiques formulées de manière formelle.

Le professeur Kevin Buzzard, de l'Imperial College London, a passé cinq ans à accomplir cette tâche, tandis que le modèle "Claude" l'a réalisée en 11 jours. Selon Buzzard, cette preuve "ne repose sur rien d'autre que les axiomes des mathématiques".

La tâche a été répartie entre des agents d'intelligence artificielle qui recevaient périodiquement des instructions générales, aidés dans la coordination de leur travail par l'outil "Prove2Me", initialement conçu pour aider les mathématiciens humains.

Si ces résultats peuvent être reproduits de manière fiable, l'intelligence artificielle pourrait accélérer considérablement le processus de traduction des mathématiques modernes en formes vérifiables automatiquement.