Formalisation du dernier théorème de Fermat dans Lean : Un projet open source collaboratif

Une collaboration internationale dirigée par Kevin Buzzard entreprend la tâche ambitieuse de prouver formellement le dernier théorème de Fermat à l'aide du vérificateur de théorèmes Lean. Financé par le Conseil de recherche en ingénierie et sciences physiques du Royaume-Uni et hébergé à l'Imperial College London, ce projet repousse les limites de la vérification des preuves mathématiques. En utilisant un ordinateur pour vérifier la preuve, le projet explore le potentiel de la formalisation et de la vérification automatisée en mathématiques, avec des implications pour les recherches futures.