Preuve du Dernier Théorème de Fermat : Les Ordinateurs Relèvent un Défi Mathématique
2024-12-12
Une équipe tente de prouver le dernier théorème de Fermat à l'aide de Lean, rencontrant des défis inattendus. Au lieu de s'appuyer sur la preuve originale, ils utilisent une approche moderne plus généralisée. Lors de la formalisation de la cohomologie cristalline, ils ont découvert une erreur dans un lemme clé, menant à une réévaluation des fondements de la théorie. Ils ont finalement trouvé une solution de contournement en utilisant une preuve différente. Cette expérience met en évidence des erreurs potentielles dans la littérature mathématique moderne et souligne la nécessité de preuves formalisées.