Ça me réjouit que Tao fasse sa conférence sur les preuves assistées par ordinateur !!! Il y a quelques mois il avait pu organiser (avec K. Buzzard notamment et il y avait aussi E. Riehl !) un séminaire sur le même sujet (ce fil peut être intéressant). Auriez vous des informations sur son rapport à un tel sujet ? S'il y a de gros projets à venir ?
J'ai l'impression que ce domaine explose (de plus en plus) (que ce soit sous l'influence de K. Buzzard ou P. Massot et cie., beaucoup d'étudiants s'intéressent à ce sujet en apprenant à programmer en Lean; il y a évidemment également Coq, Isabelle…; ou encore T. Gowers qui cherchait des doctorants et post-doctorants !; j'ai cru également lire à un endroit que Voevodsky avait lancé tout un programme sur un sujet connexe (?)). Si en plus T. Tao s'implique… ça va être merveilleux !
Lean a déjà réalisé une preuve formelle d’un théorème très technique (le théorème 9.4.de Scholze-Clausen). Visiblement, la prochaine étape serait que Lean arrive à formuler ses propres hypothèses mathématiques pour être autonome, c’est-à-dire à mimer le processus créatif d’un mathématicien.
Sinon sur son blog récemment il a fait mention d'un projet d'utilisation de l'IA pour étiqueter le cheminement d'un article. Selon une amie doctorante en géométrie algébrique c'est à la fois intéressant et réaliste.
Réponses
Ça me réjouit que Tao fasse sa conférence sur les preuves assistées par ordinateur !!!
Il y a quelques mois il avait pu organiser (avec K. Buzzard notamment et il y avait aussi E. Riehl !) un séminaire sur le même sujet (ce fil peut être intéressant).
Auriez vous des informations sur son rapport à un tel sujet ? S'il y a de gros projets à venir ?
J'ai l'impression que ce domaine explose (de plus en plus) (que ce soit sous l'influence de K. Buzzard ou P. Massot et cie., beaucoup d'étudiants s'intéressent à ce sujet en apprenant à programmer en Lean; il y a évidemment également Coq, Isabelle…; ou encore T. Gowers qui cherchait des doctorants et post-doctorants !; j'ai cru également lire à un endroit que Voevodsky avait lancé tout un programme sur un sujet connexe (?)).
Si en plus T. Tao s'implique… ça va être merveilleux !