Dans Math 2.0, Terence Tao envisage des mathématiques où les preuves deviennent plus abondantes grâce à l’IA et aux outils formels. Il souligne aussi les capacités inégales des systèmes et les difficultés persistantes à la frontière de la recherche. Son horizon dépasse la résolution de problèmes : ces outils devraient enrichir notre compréhension. Ce sont les perspectives d’un exposé, pas une mesure indépendante de performance. [1]
Une preuve de quoi ?
Lean permet de construire des preuves que son noyau vérifie à partir d’énoncés formalisés, de définitions et d’axiomes explicites. Trouver la preuve et la contrôler sont deux tâches distinctes. Mais vérifier un énoncé formel ne suffit pas à établir que cet énoncé traduit bien la question que nous voulions poser. [2]
Cette dernière distinction mérite qu’on s’y arrête. Une réponse peut être convaincante à la lecture ; une démonstration peut être correcte ; le résultat peut pourtant ne pas s’appliquer au cas qui nous intéresse. Il faut donc examiner trois choses : l’explication, la preuve et le passage de notre problème à son expression mathématique. Aucune de ces étapes ne dispense des deux autres.
Ce qu’une moyenne peut nous apprendre
Prenons un exemple élémentaire proposé ici, sans prétendre l’avoir formalisé dans Lean. Une moyenne pondérée reste entre la plus petite et la plus grande valeur si les poids sont positifs ou nuls et si leur somme est strictement positive. Cette phrase paraît presque trop familière pour qu’on examine ses conditions.
Retirons pourtant la contrainte de signe. Avec les valeurs 0 et 10, et les poids −1 et 2, la moyenne vaut (−1 × 0 + 2 × 10) / (−1 + 2), soit 20. Elle sort de l’intervalle [0, 10]. Le calcul tient sur une ligne ; il explique précisément pourquoi l’hypothèse sur les poids comptait.
Une preuve correcte du premier énoncé ne justifierait donc pas son emploi pour des coefficients négatifs. Et une preuve d’un énoncé devenu trivial par une définition trop restrictive ne nous apprendrait presque rien sur le problème initial. Avant d’admirer la réponse, il faut regarder la question exacte à laquelle elle répond.
Un instrument pour interroger
L’usage le plus intéressant à explorer serait alors de demander plusieurs objets complémentaires : un énoncé précis, une explication, des cas limites et des contre-exemples aux variantes fausses. Ces demandes n’offrent aucune garantie automatique. Elles rendent en revanche le travail contrôlable : on peut identifier une hypothèse cachée, refaire un calcul et repérer l’endroit où l’argument cesse de tenir.
Pour lire un résultat assisté par IA, je retiendrais quelques questions simples :
- Quelle question a réellement été résolue ?
- Quelles hypothèses sont indispensables, et quel exemple les met à l’épreuve ?
- Qu’est-ce qui a été vérifié, par qui ou par quel outil ?
- Que comprend-on mieux après avoir lu la preuve ?
L’enjeu ne serait pas de remplacer l’intuition par un tampon de conformité. Ce serait de mieux articuler intuition, calcul et vérification. Une machine peut aider à parcourir des pistes ; le lecteur doit encore comprendre ce qui rend une piste féconde. Le nombre de preuves produites renseignerait alors moins que la qualité des questions devenues accessibles.
Voilà la lecture que je propose de Math 2.0 : juger ces outils à ce qu’ils nous permettent de demander, de contrôler et d’expliquer. L’exemple de la moyenne est minuscule. Il rappelle pourtant une exigence qui demeure quand les outils changent : savoir exactement ce qu’on affirme, et jusqu’où cela porte.