L’IA deviendra le « copilote » des mathématiciens
L’évolution des mathématiques
- Les mathématiques ont traditionnellement été une discipline solitaire.
- Récemment, une grande partie des mathématiques est devenue suffisamment rigoureusement décomposable en éléments individuels pour pouvoir être vérifiée par ordinateur.
- Terence Tao, de l’UCLA, estime que ces méthodes ouvrent de nouvelles possibilités de collaboration en mathématiques.
L’essor des vérificateurs automatiques de preuves
- Les vérificateurs automatiques de preuves permettent aux mathématiciens de collaborer avec des centaines de personnes.
- Par exemple, Tao a démontré la conjecture Polynomial Freiman-Ruzsa (PFR) en collaboration avec plus de 20 personnes.
- Le travail avance de manière à ce que chacun apporte la preuve d’une petite étape, tandis que l’orientation d’ensemble est coordonnée.
La formalisation des mathématiques
- Il n’est pas nécessaire que tout le monde soit programmeur, et les rôles peuvent être répartis entre ceux qui se concentrent sur l’orientation mathématique et ceux qui produisent des preuves formelles.
- Le développement de bibliothèques mathématiques standard a rendu les mathématiques formelles plus pratiques.
- Un projet appelé Lean dispose d’une vaste bibliothèque comprenant des théorèmes mathématiques fondamentaux.
L’avenir de l’IA et des mathématiques
- L’IA pourrait jouer un rôle d’assistant pour les mathématiciens.
- L’IA peut aider à formaliser des preuves, à rédiger des articles et à les soumettre.
- Une collaboration est possible dans laquelle les humains fournissent les idées et l’IA les formalise.
Une nouvelle manière de faire des mathématiques
- En collaborant avec l’IA, une nouvelle manière de faire des mathématiques pourrait émerger.
- Les mathématiciens pourraient évoluer vers une répartition des rôles proche de celle de chefs de projet, tandis que l’IA aiderait à établir les preuves.
- En formalisant les manuels de mathématiques, il serait possible de créer des outils d’apprentissage plus interactifs.
Les limites et les possibilités de l’IA
- L’IA peut aider à résoudre de grands problèmes mathématiques, mais l’intuition et la compréhension humaines restent essentielles.
- Un nouveau type de mathématicien pourrait être nécessaire, capable d’analyser et de comprendre les preuves fournies par l’IA.
- L’IA peut explorer de nouveaux domaines des mathématiques et aider sur des aspects difficiles à comprendre pour les humains.
L’avis de GN⁺
- Rôle de l’IA : l’IA peut jouer un rôle important en tant qu’outil aidant les mathématiciens à résoudre des problèmes plus vastes.
- Importance de la collaboration : la collaboration entre l’IA et les humains peut ouvrir de nouvelles possibilités en mathématiques.
- Nécessité de la formalisation : la formalisation des mathématiques peut rendre davantage de connaissances explicites et favoriser la collaboration.
- Les mathématiciens de demain : un nouveau type de mathématicien pourrait être nécessaire, travaillant avec l’IA pour analyser et comprendre les preuves.
- Progrès technologique : la combinaison de l’IA et des mathématiques pourrait ouvrir encore plus de possibilités à mesure que la technologie progresse.
1 commentaires
Avis Hacker News
Texte d’Edsger Dijkstra : mention d’un texte de 1975 qui satire la manière de produire des logiciels, dont le contenu principal est une critique de la propriété intellectuelle.
Capacités des LLM : pour l’instant, ils jouent un rôle d’assistant, mais ils pourraient à l’avenir fournir un niveau d’intuition plus élevé. Par exemple, en comprenant le lien entre une bombe atomique et un tas de compost, ils pourraient repérer des éléments que les humains manquent.
Résumé de l’entretien :
Preuves vérifiées par ordinateur : l’IA peut être utile pour la vérification de preuves, comme les moteurs d’échecs. Il reste difficile de gérer un grand nombre de théorèmes et de lemmes auxiliaires, mais l’IA pourrait améliorer cela.
Histoire du logiciel et mathématiques : comparaison entre les projets logiciels du passé et l’ingénierie logicielle modulaire actuelle, avec l’idée que les mathématiques pourraient suivre un chemin similaire.
Conférence de Terence Tao : recommandation d’une conférence expliquant plus en détail comment utiliser Lean dans la recherche en mathématiques.
Preuves mathématiques avec GPT-4 : présentation d’un cas où GPT-4 a réussi à démontrer un nouveau lemme auxiliaire. Cela pourrait être utile pour la recherche mathématique.
Jeunes mathématiciens et Lean : avis selon lequel, en début de carrière, il peut être préférable de faire confiance à son intuition et de rédiger des articles.
Apprendre de l’échec : avis selon lequel apprendre des échecs des autres est très productif.