FROM INTUITION TO RESEARCH
Trois niveaux de compréhension
01 · Comprendre le problème
Pour n supérieur à deux, aucun entier positif a, b, c ne satisfait aⁿ + bⁿ = cⁿ. Le théorème était déjà démontré ; Claude l'a formalisé.
02 · Comprendre la contribution
Anthropic annonce une formalisation Lean complète en onze jours, commentée par Kevin Buzzard.
03 · Contexte académique
Il s'agit d'autoformalisation, non de la résolution d'une conjecture ouverte. Le noyau Lean vérifie des termes de preuve relativement à leurs axiomes et définitions.
Ce qui pourrait changer
Vers une vérification plus accessible des longues démonstrations.
Ce qui n'est PAS établi
Le théorème avait déjà été prouvé par Andrew Wiles.