Un relais qui s'étend sur plus de 300 ans : Inspirés par Terence Teru, des mathématiciens ont décidé d'utiliser l'IA pour formaliser la preuve du dernier théorème de Fermat.

Inspirés par Terence Tao, de plus en plus de mathématiciens commencent à essayer d'utiliser l'intelligence artificielle pour l'exploration mathématique. Cette fois, leur objectif est le dernier théorème de Fermat, l'un des dix problèmes mathématiques les plus difficiles au monde. Le dernier théorème de Fermat est un problème mathématique très complexe pour lequel aucune solution réalisable n'a été trouvée jusqu'à présent. Les mathématiciens espèrent qu'avec la puissante puissance de calcul et les algorithmes intelligents de l'intelligence artificielle, ils pourront explorer en mathématiques

Le dernier théorème de Fermat, également connu sous le nom de « dernier théorème de Fermat (FLT) », a été inventé au XVIIe siècle. Proposé par les Français le mathématicien Pierre de Fermat. Il y a une histoire légendaire derrière cela. On raconte que vers 1637, alors que Fermat lisait la traduction latine de l'Arithmétique de Diophante, il écrivit à côté de la proposition 8 du tome 11 : « Divisez un nombre cubique par la somme de deux nombres cubes, ou Il est impossible de diviser un quatrième puissance en somme de deux puissances quatrièmes, ou généralement une puissance supérieure à la puissance seconde en somme de deux puissances de même puissance. "Je suis convaincu d'avoir découvert quelque chose à ce sujet. C'est une démonstration merveilleuse, mais malheureusement la. l'espace vide ici est trop petit pour l'écrire. "

Ce qui est indiqué dans ce paragraphe est le contenu du dernier théorème de Fermat : lorsque l'entier n>2, l'équation sur x^n + y^n=z^n n'a pas de solution entière positive.

Fei Ma a dit qu'il savait comment le prouver, mais il ne l'a pas écrit parce que l'espace vide dans le livre était trop petit. Il y a eu plus tard une controverse sur l'authenticité de l'histoire et sur la question de savoir si Fermat avait vraiment compris la méthode de preuve. Depuis plus de 300 ans, les mathématiciens ont travaillé dur pour prouver le dernier théorème de Fermat. Ce n'est qu'en 1995 que le professeur Andrew Wiles de l'université de Princeton aux États-Unis a finalement achevé la preuve en 130 pages.

Maintenant que le dernier théorème de Fermat a été prouvé, que peuvent faire d'autre les mathématiciens avec l'IA ? La réponse est : formaliser sa preuve

La formalisation en mathématiques y fait généralement référence. et théorie des ensembles) pour exprimer des objets mathématiques, des structures, des théorèmes et des preuves afin qu'ils puissent être représentés, vérifiés et exploités sur des ordinateurs, garantissant ainsi l'exactitude et la cohérence du contenu mathématique. Le développement des mathématiques remonte à la fin du XIXe siècle. début du XXe siècle, tandis que les mathématiques formelles modernes ont commencé avec le développement de la logique mathématique et de l'informatique au XXe siècle. L'objectif principal des mathématiques formelles est d'établir un système formel comprenant un ensemble de symboles, un ensemble d'axiomes de base et un ensemble de règles de raisonnement. Grâce à l'utilisation de ces règles et axiomes, il est possible de réaliser

At. À la fin de l'année dernière, Tao Zhexuan et d'autres ont utilisé Lean (un prouveur de théorèmes interactif et un langage de programmation) pour formaliser l'un de leurs articles. L'article, une preuve d'une version de la conjecture polynomiale de Freiman-Ruzsa, a été publié sur arXiv en novembre dernier. Lors de l'écriture du code en langage Lean, Tao Zhexuan a également utilisé l'assistant de programmation IA Copilot. Cet incident a attiré une large attention dans les communautés des mathématiques et de l’intelligence artificielle.

A cette époque, Kevin Buzzard de l'Imperial College de Londres, le plus important promoteur de la communauté open source de la technologie Lean, déclarait : « Fondamentalement, il est évident que lorsque vous numérisez quelque chose, vous pouvez l'utiliser de nouvelles manières. va numériser les mathématiques, ce qui rendra les mathématiques meilleures."

Ce professeur Buzzard est le mathématicien qui a récemment prétendu formaliser la preuve du dernier théorème de Fermat, et l'outil qu'il a utilisé est aussi Lean.

Dans un blog, il a présenté le contexte, la motivation et les méthodes spécifiques pour y parvenir.

Pourquoi formaliser la preuve du dernier théorème de Fermat ?

La forme du dernier théorème de Fermat est très simple et intuitive, mais sa démonstration est extrêmement difficile. C’est sans aucun doute une excellente démonstration de la profonde beauté des mathématiques. Au cours des derniers siècles, afin de résoudre ce problème, les mathématiciens ont développé et innové un grand nombre de théories mathématiques, qui ont des applications dans des domaines allant de la cryptographie à la physique.

Andrew Wiles a peut-être été inspiré par FLT, mais ses travaux ont en fait conduit à une percée dans le projet Langlands, une série d'idées mathématiques de grande envergure qui liaient la théorie des nombres, la géométrie algébrique et la théorie de la représentation de groupe réduite, et qui continueront à le faire. attirer beaucoup d’attention en 2024.

Historiquement, plusieurs autres avancées majeures dans la théorie algébrique des nombres (telles que la théorie de la factorisation dans les champs numériques et l'arithmétique dans les champs cycliques) ont été au moins en partie motivées par le désir d'une compréhension plus approfondie de la FLT.

Le travail de Wiles, complété par son élève Richard Taylor, s'appuie sur une vaste base de mathématiques du 20e siècle. La technique de base introduite par Wiles - le « théorème de levage de modularité » - a été conceptuellement considérablement simplifiée et largement généralisée au cours des 30 années qui ont suivi la publication de l'article original. Ce domaine est encore très actif aujourd’hui. Article de Frank Calegari au Congrès international des mathématiciens 2022, décrivant les progrès réalisés depuis la percée de Wiles (voir : https://arxiv.org/abs/2109.14145). Kevin Buzzard a déclaré que la poursuite de son activité dans ce domaine était l'une de ses motivations pour formaliser la preuve FLT.

Formalisation des mathématiques, l'art de convertir les mathématiques sur papier en un langage de programmation informatique capable de comprendre des théorèmes et de prouver des concepts. Ces langages de programmation, également connus sous le nom de prouveurs de théorèmes interactifs (ITP), existent depuis des décennies. Ces dernières années, ce domaine semble toutefois avoir attiré l’attention de la communauté mathématique. Nous avons assisté à plusieurs exemples de formalisation de la recherche en mathématiques, le dernier en date étant la formalisation de la preuve de la conjecture polynomiale de Freiman-Ruzsa par Terence Tao et d'autres. Cet article révolutionnaire de 2023 a été formalisé en Lean en seulement trois semaines. De telles réussites pourraient amener les observateurs à penser que les ITP comme Lean sont désormais prêts à formaliser toutes les mathématiques modernes.

Cependant, la vérité est loin d’être aussi simple. Dans certains domaines des mathématiques, comme la combinatoire, nous pouvons voir certaines avancées modernes se formaliser en temps réel. Cependant, Buzzard a déclaré qu'il assistait régulièrement à des séminaires de théorie des nombres à Londres et remarquait souvent que les connaissances de Lean sur les définitions mathématiques modernes étaient insuffisantes pour formuler les résultats annoncés lors des séminaires, et encore moins pour vérifier leurs preuves.

En fait, le « décalage » dans cet aspect de la théorie des nombres était l'une des principales motivations de Buzzard pour lancer la formalisation de la preuve contemporaine de FLT. À la fin du projet, Lean sera capable de comprendre les formes et représentations automorphes (une classe spéciale de fonctions de variables complexes), les représentations de Galois, l'automorphisme latent, les théorèmes de promotion de la modularité, l'arithmétique des variétés algébriques, la théorie des champs de classes, les théorèmes des duaux arithmétiques. , variétés Shimura et autres concepts utilisés dans la théorie algébrique moderne des nombres. Selon Buzzard, une fois ces fondations en place, formaliser ce qui se passe dans son propre domaine d'expertise ne relèvera plus de la science-fiction.

Alors, pourquoi fais-tu ça ? Buzzard explique : "Si l'on en croit certains informaticiens, la croissance exponentielle de l'intelligence artificielle permettra à terme aux ordinateurs d'aider les mathématiciens dans leurs recherches. De tels travaux peuvent aider les ordinateurs à comprendre ce que nous faisons dans la recherche mathématique moderne." le projet?

Le projet de formalisation du dernier théorème de Fermat est désormais lancé. Buzzard montre les progrès actuels dans un graphique.

Les chercheurs intéressés peuvent lire les détails : https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

Le projet est financé par l'EPSRC et Buzzard recevra un soutien financier pendant les cinq premières années. Durant cette période, son premier objectif était de réduire la FLT à une formule connue des mathématiciens à la fin des années 1980.

Bien sûr, Buzzard n’avait pas l’intention de faire cela seul. Il a déclaré que pour certaines parties de l’argumentation, il comprenait les principes de base mais n’avait jamais examiné les détails en détail. De plus, le projet Langlands a également introduit des éléments importants, notamment la transformation de base cyclique de GL_2 et Jacquet-Langlands. Sa compréhension de ces choses profondes n’est pas assez profonde.

Cependant, c'est précisément l'avantage des projets formels. Buzzard sera capable d'articuler les résultats dont il a besoin en Lean et de les communiquer aux autres. La beauté de ce système est la suivante : vous n’avez pas besoin de comprendre l’intégralité de la preuve de FLT pour contribuer. Le diagramme ci-dessus divise la preuve en plusieurs petits lemmes, ce qui la rend très pratique pour le crowdsourcing. Si vous pouvez prouver formellement l'un de ces lemmes, Buzzard attendra avec impatience votre pull request.

Ceux qui souhaitent participer au projet doivent connaître quelque chose sur le Lean. Pour cela, Buzzard recommande le manuel en ligne Mathematics in Lean.

Lien du manuel : https://leanprover-community.github.io/mathematics_in_lean/

Ce projet sera mené sur le flux FLT du chat Lean Zulip, un puissant forum de recherche pour les mathématiciens et les informaticiens. en temps réel, publiez facilement du code et des mathématiques et utilisez des systèmes de threading et de flux pour prendre en charge efficacement plusieurs conversations indépendantes en même temps.

Lien de discussion Lean Zulip : https://leanprover.zulipchat.com/

Buzzard a déclaré qu'il n'avait aucune idée de la durée du projet, mais il est définitivement optimiste.

Dans le même temps, les outils de preuve formelle comme Lean sont également en constante itération. Par rapport au Lean original, la dernière version Lean 4 présente de nombreuses optimisations, notamment un compilateur plus rapide, une gestion améliorée des erreurs et une meilleure intégration avec des outils externes.

À la fin de l'année dernière, l'équipe de la plateforme ouverte LeanDojo et des chercheurs de Caltech ont également lancé Lean Copilot, un outil de collaboration conçu pour permettre aux grands modèles de langage d'interagir avec les humains, injectant la puissance des grands modèles d'IA dans la recherche mathématique.

"Je prédis que, si elle est utilisée correctement, l'IA deviendra un co-auteur de confiance dans la recherche mathématique et dans de nombreux autres domaines d'ici 2026", a déclaré Terence Tao dans un blog précédent.

J’espère que la prédiction de Terence Tao se réalisera bientôt.

Lecture connexe :

• 《Quelle est la preuve formelle de Terence Tao utilisant l'IA ? Comprenez la vie passée et présente de la conjecture PFR dans un seul article》

• 《L'assistant de preuve préféré de Tao Zhexuan, Lean, utilise de grands modèles》

• 《Les grands modèles aident Tao Zhexuan à résoudre des problèmes et à prouver des théorèmes mathématiques : Les mathématiques sont vraiment importantes. Sont-elles devenues la première discipline à réaliser une percée grâce à l’IA ? 》

• 《Nouveau projet de Tao Zhexuan : prouver le théorème des nombres premiers en Lean, le plan de recherche est prêt》

^{Lien de référence : https://leanprover.zulipchat.com/#narrow/ flux /416277-FLT}

^{https://mp.weixin.qq.com/s/d9RSkRhlKH5ZMek3yTqe4Q}

Ce qui précède est le contenu détaillé de. pour plus d'informations, suivez d'autres articles connexes sur le site Web de PHP en chinois!