Terence Tao donne à Caltech une conférence « Math 2.0 » sur les preuves par machine

Terence Tao a publié l'enregistrement de sa conférence « Math 2.0 » (« Mathématiques 2.0 »), donnée au California Institute of Technology. Il a commencé à préparer cette intervention il y a plus d'un an et l'appelait alors « Machine Assisted Proof », c'est-à-dire « preuve assistée par machine ». La conférence devait avoir lieu en mai, mais elle a été reportée à octobre. Selon Tao, la raison tient à plusieurs événements récents. L'extrait disponible ne dit pas lesquels. Le média chinois Jiqizhixin a mis en titre l'idée centrale : le temps où les preuves manquaient touche à sa fin.

Ce que l'on sait de la conférence

Le changement de titre est en soi révélateur. Il y a un an, le sujet était présenté comme un outil : l'ordinateur aide à vérifier et à trouver des preuves. À l'automne 2026, l'auteur retient la formule « Mathématiques 2.0 », ce qui renvoie à un changement de la pratique elle-même. Tao ne l'explique pas en une phrase : il renvoie à l'enchaînement des événements de ces derniers mois. Mieux vaut consulter le texte intégral et les diapositives à la source, car le compte rendu s'interrompt précisément là où commence le fond.

Données clés de l'extrait disponible :

• format : conférence publique à Caltech, enregistrement publié le 11 octobre 2026 ;
• titre de travail lors de la planification : « Machine Assisted Proof » ;
• titre final : « Math 2.0 » ;
• calendrier : initialement mai 2026, en pratique octobre ;
• temps de préparation : plus d'un an.

D'où vient la thèse de la fin de la rareté

L'idée que les preuves cessent d'être une denrée rare n'est pas sortie de nulle part. Ces dernières années, Tao travaille publiquement à la jonction des mathématiques et des machines. Fin 2023, il a dirigé la formalisation, dans le système Lean, de la preuve de la conjecture PFR (conjecture polynomiale de Freiman–Ruzsa).

Le projet a réuni une équipe distribuée et pris plusieurs semaines. En 2024, le modèle AlphaProof de Google DeepMind a résolu des problèmes de l'Olympiade internationale de mathématiques au niveau d'une médaille d'argent. En 2025, Tao a participé aux tests d'AlphaEvolve sur des dizaines de problèmes ouverts d'analyse et de combinatoire.

Tout cela relève du contexte antérieur et non du contenu de la nouvelle conférence, mais cela dessine une trajectoire. D'abord, la vérification des preuves passe à la machine, puis une partie de la recherche suit.

En mathématiques classiques, la rareté de la preuve déterminait tout. Un théorème avait de la valeur en partie parce qu'il avait coûté des années de travail humain, et que sa vérification par un relecteur prenait elle aussi du temps. Si la génération et la vérification deviennent moins chères, l'économie de la discipline change aussi. La valeur se déplace de la preuve elle-même vers la formulation des questions, le choix des directions et la compréhension de l'utilité d'un résultat.

Où se situe la limite

Le titre de Jiqizhixin est tranché, alors que Tao multiplie d'ordinaire les réserves. La formalisation en Lean exige un travail considérable, et les modèles de langage peuvent se tromper avec aplomb. La recherche automatique fonctionne bien là où le résultat se vérifie mécaniquement. Il est donc raisonnable d'attendre de « Math 2.0 » qu'elle décrive non pas le remplacement des mathématiciens, mais une nouvelle division du travail. Il s'agit toutefois d'une hypothèse, pas d'un résumé de la conférence : cette conclusion ne figure pas dans le texte disponible.

Comment l'utiliser en pratique

Pour les chercheurs et ingénieurs qui suivent le sujet, trois étapes sont utiles. Premièrement, regarder l'enregistrement en entier et y confronter tout compte rendu de seconde main, y compris celui-ci. Deuxièmement, se former à Lean et à la bibliothèque Mathlib : c'est sur cette infrastructure que reposent les projets dont parle Tao. Troisièmement, pour les équipes qui développent de l'IA pour la science, la vérifiabilité sert de repère. Les modèles dont les sorties se vérifient automatiquement prennent un avantage net sur ceux qui produisent un texte simplement plausible.

Pour l'instant, la conférence est publiée et sa thèse principale reste matière à lecture et à débat. Si Tao a raison, les prochaines années le montreront par un déplacement de ce que les revues et les conférences jugent digne d'être publié.