Anthropic affirme que Claude a aidé à formaliser le dernier théorème de Fermat dans Lean

Anthropic a publié une recherche décrivant comment Claude a été utilisé pour aider à formaliser le dernier théorème de Fermat dans Lean, un assistant de preuve qui vérifie les arguments mathématiques étape par étape. L’annonce ne signifie pas que le modèle a découvert seul une nouvelle preuve. Elle montre plutôt une frontière pratique de l’IA en mathématiques: transformer des preuves humaines très condensées en code formel vérifiable par une machine.

Le dernier théorème de Fermat est l’un des résultats les plus célèbres de l’histoire des mathématiques. Andrew Wiles l’a démontré dans les années 1990, mais sa preuve repose sur des outils profonds de théorie des nombres et de géométrie algébrique. Formaliser un résultat de cette ampleur est très différent d’une explication en prose. Chaque définition, dépendance, transformation et étape logique doit être assez explicite pour être acceptée par l’assistant de preuve. Même pour des spécialistes, c’est un travail lent et exigeant.

Anthropic présente Claude comme un collaborateur dans ce processus d’ingénierie de preuve. Le modèle peut proposer du code Lean, traduire des énoncés mathématiques en syntaxe formelle, corriger des erreurs et suggérer des façons de relier des lemmes intermédiaires. Les chercheurs doivent toujours décider si une voie est mathématiquement solide, relire le code généré et guider le système lorsque l’état de preuve devient complexe. Le résultat illustre donc un progrès de l’assistance IA, pas la disparition du jugement humain.

La preuve formelle est un test difficile pour les modèles de langage. Un modèle peut produire un texte convaincant tout en étant faux, alors que Lean n’accepte pas une preuve dont la logique ne se vérifie pas. Cela crée une boucle de rétroaction où de nombreuses erreurs sont détectées automatiquement. Le succès se mesure autrement: il ne s’agit plus seulement d’écrire un beau paragraphe de preuve, mais d’aider à construire des artefacts vérifiables dans un système strict.

Pour l’industrie de l’IA, cette recherche indique une voie plus mature pour les sciences et les techniques. Les modèles peuvent prendre en charge des boucles fastidieuses de traduction, recherche et réparation, accélérant le travail d’équipes expertes. Les mathématiques formelles, la vérification de programmes et l’ingénierie critique exigent plus qu’un texte fluide. Elles demandent des chaînes de raisonnement auditables et des résultats contrôlables par des outils externes.

Anthropic présente ce travail comme une étape, non comme un aboutissement. Formaliser de grands théorèmes reste difficile et dépend encore de la planification et de la correction humaines. Mais la publication renforce une tendance: les systèmes d’IA de pointe sont de plus en plus évalués sur leur capacité à produire des travaux vérifiables dans des environnements exigeants.