L’IA “formalise” le dernier théorème de Fermat en seulement onze jours

Une démonstration “formalisée” du dernier théorème de Fermat a été élaborée par un prototype avancé du modèle d’intelligence artificielle (IA) Claude. C’est ce qu’a annoncé, le 4 septembre, Anthropic, l’entreprise qui l’a développé.

Cette semaine, nos articles sont

dans l’application

“Il n’a fallu que 11 jours à plusieurs agents d’IA [travaillant ensemble] pour accomplir cette mission et confirmer que la preuve apportée par un humain dans les années 1990 était correcte”, rapporte l’hebdomadaire New Scientist. Le dernier théorème de Fermat, énoncé en 1637 par le mathématicien français Pierre de Fermat, avait obsédé les esprits les plus brillants pendant des siècles jusqu’à ce qu’Andrew Wiles en apporte la démonstration en 1995.

Son énoncé est assez simple. Il stipule qu’il n’existe pas de nombre entier positif a, b et c qui vérifient l’équation suivante : aⁿ + bⁿ = cⁿ, où n est un entier supérieur à 2. Si sa démonstration particulièrement complexe a pris du temps, la méthode pour la traduire en langage informatique n’avait pas encore été trouvée.

Or, depuis quelques mois, l’IA accomplit des progrès phénoménaux dans toutes les branches des mathématiques, longtemps considérées comme l’apanage du génie humain. Désormais, assure Nature, “des IA sont notamment capables de ‘formaliser’ des démonstrations, c’est-à-dire de traduire des arguments mathématiques formulés en langage naturel en des lignes de code vérifiables par ordinateur, généralement dans le langage de programmation Lean”.