Des chercheurs se sont réunis à Londres cette semaine pour accélérer la formalisation du dernier théorème de Fermat à l'aide de modèles d'IA avancés. L'atelier se concentre sur la conversion de la démonstration d'Andrew Wiles de 1993 en code Lean pour une vérification informatique. Les progrès ont été rapides, le nombre de lignes de code ayant doublé après le premier jour.
Vingt-cinq mathématiciens, informaticiens et experts en IA se sont réunis dans un hôtel du centre de Londres pour travailler sur le projet dirigé par Kevin Buzzard de l'Imperial College de Londres. Ce projet quinquennal, financé en 2024, vise à ajouter le théorème au dépôt Mathlib de mathématiques formalisées.
Avant l'atelier, le projet comptait 20 000 lignes de code. Après le premier jour, le total atteignait 40 000. Kevin Buzzard a noté que les capacités de l'IA se sont nettement améliorées depuis décembre dernier, permettant à l'équipe de traiter une plus grande partie des mathématiques sous-jacentes que ce qui était initialement prévu.
Hang Lu Su, également de l'Imperial College de Londres, a décrit le processus comme une industrialisation du travail intellectuel. Les participants utilisent des modèles, notamment Claude, pour générer et affiner le code, bien que des inquiétudes subsistent concernant la prolixité et la maintenabilité à long terme des résultats produits par l'IA.
Kevin Buzzard s'est montré confiant quant au respect des objectifs initiaux d'ici la fin du projet. L'avancement de l'équipe sur la pyramide complète des théorèmes de soutien dépendra des futurs développements de l'IA.