INTELLIGENCE ARTIFICIELLE –  Mathématiques : Claude réalise en 11 jours un travail estimé à dix ans pour des humains

L’IA d’Anthropic a transformé la démonstration du dernier théorème de Fermat en une preuve entièrement vérifiable par ordinateur. Une opération achevée en onze jours, alors qu’un travail humain comparable était estimé à environ dix ans.

Claude n’a pas résolu le dernier théorème de Fermat. Andrew Wiles l’avait déjà démontré dans les années 1990. La performance annoncée par Anthropic est différente : son système d’intelligence artificielle a traduit cette démonstration mathématique extrêmement complexe dans Lean, un langage permettant à un ordinateur de contrôler chaque étape logique d’une preuve.

Le résultat donne la mesure de l’accélération. Claude a travaillé largement de manière autonome pendant 11 jours, produit environ 13 millions de lignes de code Lean et utilisé quelque 29 500 théorèmes intermédiaires pour parvenir à une démonstration complète vérifiable par machine.

Pourquoi aurait-il fallu près de dix ans à des humains ?

Selon Nature, ce chantier était considéré comme susceptible de demander environ dix années de travail humain. Cette estimation s’explique par la nature même de la formalisation.

Un mathématicien écrivant pour d’autres spécialistes peut omettre des étapes considérées comme évidentes. Un logiciel de vérification, lui, n’accepte aucun raccourci. Chaque définition, chaque propriété utilisée et chaque enchaînement logique doivent être explicités dans un langage que la machine peut contrôler.

Il ne suffit donc pas de recopier les 129 pages de la démonstration de Wiles. Il faut reconstruire tout l’édifice sous une forme informatique rigoureuse, parfois en formalisant au passage des résultats mathématiques qui ne l’avaient jamais été auparavant. Anthropic souligne que ce travail devait initialement prendre plusieurs années.

Une accélération potentiellement majeure pour la recherche

La portée dépasse le théorème de Fermat. Si les IA deviennent capables de formaliser rapidement des travaux scientifiques, elles pourraient aider les chercheurs à détecter des erreurs, vérifier des démonstrations complexes et contrôler des résultats nouveaux.

L’enjeu est particulièrement important à mesure que l’IA elle-même produit davantage de raisonnements mathématiques. Les chercheurs pourraient disposer d’un outil capable non seulement de proposer des solutions, mais aussi de transformer leurs démonstrations en objets contrôlables automatiquement.

La performance ne remplace donc pas le mathématicien qui découvre et comprend. Elle pourrait en revanche réduire radicalement le temps nécessaire pour vérifier que son raisonnement tient réellement debout.