-
Projet Xena et dernier théorème de Fermat
- Le projet Xena vise à formaliser les mathématiques sur ordinateur. L’objectif est que, si une révolution de l’IA en mathématiques se produit, les ordinateurs puissent aider à étendre les frontières de la théorie moderne des nombres.
-
Formalisation du dernier théorème de Fermat
- Un travail est en cours pour démontrer sur ordinateur le dernier théorème de Fermat (FLT). Dans ce processus, l’un des principaux défis consiste à enseigner à l’ordinateur le théorème R=T.
- Plutôt que la preuve originale de Wiles, l’objectif est de formaliser une preuve moderne, généralisée et simplifiée.
-
Cohomologie cristalline et structures à puissances divisées
- La cohomologie cristalline est une théorie développée dans les années 1960-70, qui joue un rôle important dans la formalisation mathématique.
- Les structures à puissances divisées sont un concept nécessaire pour enseigner la cohomologie cristalline à l’ordinateur.
-
Le problème de la documentation mathématique humaine
- Cela met en lumière le manque de précision de la documentation mathématique. C’est quelque chose de connu parmi les spécialistes, mais qui est souvent mal documenté.
- Le travail de formalisation peut aider à résoudre ce problème.
-
Importance de la formalisation
- Formaliser les mathématiques est une étape importante pour permettre aux machines de construire elles-mêmes des raisonnements mathématiques.
- De nombreux mathématiciens ne perçoivent pas la nécessité de la formalisation, mais elle est essentielle pour réduire les erreurs humaines.
-
Conclusion
- Lors d’une récente présentation, le problème de la formalisation des puissances divisées a été résolu. Cela signifie que le projet est de nouveau sur les rails.
1 commentaires
Avis sur Hacker News
Se remémore son expérience de l’école doctorale, lorsqu’il écrivait du code rapide pour aider à explorer la conjecture de Birch et Swinnerton-Dyer. Quand il a dit en séminaire qu’il voulait trouver un contre-exemple, les experts se sont mis en colère. Il ne comprenait pas la profondeur des mathématiques, mais sa curiosité en a été stimulée.
Se réjouit des progrès du formalisme en mathématiques. En tant que programmeur, cela rend les mathématiques plus accessibles. L’inquiétude face au manque de formalisme doit être affrontée par la curiosité.
Les mathématiciens ont souvent tendance à omettre des détails. Si l’on veut des preuves rigoureuses, on a besoin de l’aide d’experts. Les mathématiques modernes reposent sur des bases fragiles.
Se remémore le processus par lequel Andrew Wiles a démontré FLT. La manière de prouver dans les années 1990 semble déjà ancienne.
Souligne le manque de documentation des mathématiques modernes. Il faut réduire les erreurs grâce aux systèmes formels. Il est important d’enseigner les raisonnements mathématiques aux machines.
Explique la différence de rôle entre les designers UI/UX et les développeurs. Le design et le développement exigent des façons de penser différentes.
Espère que des assistants de preuve comme Lean deviendront des outils importants en mathématiques.
Trouve intéressant d’examiner du code Lean. L’énoncé final de la preuve joue le rôle d’un test unitaire.
S’interroge sur la possibilité que des concepts mathématiques utilisés depuis des décennies soient erronés.
Présente le mot « vitiated » en disant qu’il est utile à employer lorsqu’une preuve est erronée.
Mentionne l’écart entre mathématiciens et ingénieurs, et s’attend à ce qu’il faille aussi des gains de performance lorsque les machines résoudront des problèmes mathématiques.
Exprime sa déception face à l’état de la littérature mathématique. Il s’attend à trouver des problèmes dans la littérature de théorie des nombres des années 1960 à 1990. Plus une communauté d’experts est petite, plus les erreurs peuvent passer inaperçues.