Trop de preuves générées par l'IA ne sont pas nécessairement une bonne chose... Le monde des mathématiques a du mal à tout lire.
Mais la bonne nouvelle est que——
Face à cette crise, deux lauréats de la médaille Fields, Tao Zhexuan et Wang Hong, portent un jugement quasiment identique :
Digérer.
La faculté de mathématiques de l'Université de Pékin a récemment publié une longue interview de Wang Hong, dans laquelle elle donne un conseil assez mesuré :
Le monde des mathématiques ne peut pas ignorer les contre-exemples ou preuves générés par l'IA, nous devons apprendre à les utiliser, mais aussi les comprendre et les digérer.
Quant à Tao Zhexuan, il a passé plusieurs jours à digérer complètement une preuve réalisée avec la participation de l'IA, du début à la fin.
Cette preuve résout précisément la conjecture de Sendov, en suspens depuis 67 ans.
Cela semble un peu contre-intuitif. Si l'IA est là pour aider les mathématiciens à résoudre des problèmes et que la réponse est déjà trouvée, pourquoi faut-il encore la digérer ?
La réponse donnée par le « lanceur d'alerte » Tao Zhexuan est :
Une preuve correcte n'est que la première étape d'un résultat mathématique ; elle doit encore être comprise et assimilée par des mathématiciens professionnels pour être pleinement utilisable.
Pour faire une analogie, un auteur traditionnel est comme un parent responsable, accompagnant une preuve de sa naissance à sa publication. Désormais, danser avec l'IA, cette relation pourrait plutôt ressembler à une « adoption » :
Quelqu'un utilise l'IA pour faire progresser une preuve jusqu'à sa génération ou sa vérification, puis passe officiellement le relais à un autre groupe pour l'interprétation professionnelle, la mise en forme et la publication.
Les mathématiciens ont encore beaucoup à faire.
La digestion est la prochaine étape pour résoudre la crise séculaire des mathématiques
En clair, c'est aussi la réponse de Tao Zhexuan à la question qu'il a laissée un mois plus tôt dans sa conférence au CIM :
Si les réponses peuvent être produites en masse par l'IA, que doit encore rechercher la recherche mathématique ?
Le nouveau modèle Astra d'OpenAI a résolu 10 problèmes difficiles en mathématiques et en informatique théorique, couvrant la géométrie en haute dimension, la théorie des codes, la théorie des groupes, entre autres.
Un neurochirurgien sans formation mathématique avancée a laissé ChatGPT 5.6 fonctionner de manière autonome pendant environ 16 heures, obtenant une preuve clé de la conjecture de Crouzeix en algèbre linéaire numérique.
......
Le haut mur des mathématiques semble s'être vu percer une porte dérobée par l'IA.
Même des profanes peuvent, grâce à elle, percer des problèmes de pointe. Les mathématiques seraient-elles en train de suivre le scénario du « prochain génie civil » ? (doge)
Non ! En réalité, un résultat mathématique complet ne se limite jamais à l'étape de « l'obtention d'une preuve ».
Tao Zhexuan le divise en cinq étapes :
D'abord générer l'argumentation, puis vérifier sa justesse ; ensuite, il faut expliquer l'idée à ses pairs, la soumettre à la publication et à l'examen par la communauté ; enfin, il faut réorganiser le résultat, trouver ses liens avec les théories existantes, et le consolider en une connaissance standard utilisable par la suite.
L'IA excelle actuellement à accélérer les deux premières étapes. Plus on avance, plus il faut le jugement du mathématicien pour déterminer le cœur du problème et la signification du résultat.
Et la conjecture de Sendov que Tao Zhexuan vient de traiter est presque une mise en pratique à l'identique de ce processus.
Cette conjecture étudie la distance entre les zéros d'un polynôme et ses points critiques. Les cas de degré faible et de degré suffisamment grand avaient déjà été résolus, laissant un vide persistant pour les degrés intermédiaires.
Il y a quelques jours, l'amateure de mathématiques Lech Mazur a utilisé l'IA pour combler cette lacune, fournissant une preuve formalisée vérifiée par Lean.
L'histoire semblait devoir s'arrêter là. Mais Tao Zhexuan a remarqué que cette preuve originale n'avait pas encore été mise en forme dans un texte mathématique adapté à la lecture et à la publication par des humains. En d'autres termes, le résultat mathématique n'était pas encore utilisable.
Il a donc passé plusieurs jours, avec l'aide conjointe de ChatGPT et de déductions sur papier, à procéder à une digestion complète du résultat :
Retracer les sources bibliographiques → Extraire les identités réellement opérantes → Supprimer les détours → Réécrire l'argumentation découverte par la machine en une version faisant ressortir la ligne directrice.
Cette lecture a même fait émerger de nouveaux éléments.
L'argumentation remise en forme ne résout pas seulement la conjecture de Sendov, mais peut aussi couvrir la conjecture plus forte de Phelps–Rodriguez. Les outils fondamentaux nécessaires sont aussi plus élémentaires que ce que la présentation formalisée originale laissait supposer, le code Lean passant d'environ 90 000 lignes à 15 000 lignes.
En d'autres termes, digérer n'est pas seulement une revérification de la preuve de l'IA, c'est aussi un moyen efficace d'élargir les résultats mathématiques.
Surtout, Tao Zhexuan souhaite, grâce à cette digestion, renverser l'ancienne règle du monde mathématique selon laquelle « celui qui annonce en premier obtient la priorité ».
L'attribution des résultats mathématiques s'est d'abord faite sur la date de publication dans les revues, puis sur l'horodatage arXiv.
Aujourd'hui, les preuves de l'IA arrivent trop vite, même arXiv est jugé trop lent, certains résultats étant balancés sur les réseaux sociaux dès leur génération. Pour devancer les autres, vérification et interprétation sont toutes sautées, créant finalement une charge de travail artificielle pour la communauté mathématique.
C'est pourquoi, dans sa conférence au CIM, Tao Zhexuan a plaidé pour que le monde mathématique cesse de glorifier sans cesse « le premier à donner une preuve », et qu'il rehausse le statut de « la digestion et la mise en forme des preuves ».
Expliquer une preuve, la relire, intégrer un résultat dans la théorie classique, ces travaux doivent aussi être valorisés ; on ne peut pas considérer que seule la production de nouveaux théorèmes mérite des mérites.
Si les auteurs d'un article ne sont pas capables de faire une présentation au niveau expert pour expliquer clairement leurs résultats, même si l'IA les a vérifiés comme corrects, ce résultat ne devrait pas être publié.
Une preuve incompréhensible par l'humain ne peut être considérée comme un résultat complet.
C'est pourquoi Tao Zhexuan appelle la communauté à s'asseoir calmement pour mener une discussion profonde sur les limites de l'IA, les valeurs des mathématiques, tout en soulignant les aspects du travail mathématique qui ne peuvent être remplacés par la machine.
Encore une chose
Parallèlement, Tao Zhexuan a aussi concrètement rendu public un référentiel pour enregistrer les résultats vérifiés par Lean – Palomar.
Palomar enregistre clairement l'énoncé du problème, le code de la preuve, le mode et la version de participation de l'IA, puis effectue une vérification indépendante par un noyau, rassemblant au même endroit les preuves de l'IA dispersées sur GitHub, les réseaux sociaux et dans les actualités.
Il servira de station relais de digestion entre la vérification et la publication, permettant à ceux qui suivent de savoir où en sont l'IA et leurs pairs, et quels travaux restent à accomplir.
Les équipes intéressées par un même problème peuvent collaborer via Palomar.
Il est important de noter que Palomar ne se charge pas d'annoncer l'importance d'un résultat, ni de remplacer l'examen par les pairs.
À l'avenir, la priorité sur un résultat spécifique sera déterminée conjointement par l'ordre chronologique de quatre jalons :
La génération du résultat documentant comment la preuve a été produite, comme les historiques de chat de l'IA ;
La vérification du résultat confirmant la justesse logique, comme le code Lean ;
L'interprétation du résultat expliquant clairement l'idée, comme une conférence publique ;
La publication formelle du résultat, comme un article.
En d'autres termes, la priorité revient à celui qui fournit le premier un ensemble complet de résultats.
Actuellement, la conjecture de Sendov remise en forme par Tao Zhexuan fait partie des premiers dossiers de Palomar.
Références :
[1]https://arxiv.org/abs/2608.16753
[2]https://mathstodon.xyz/@tao/117123957813926355
[3]https://www.youtube.com/watch?v=M0--ZH1lOzg
[4]https://mp.weixin.qq.com/s/w-UfVMmwTZqXjNsC81CzYw
Cet article provient du compte WeChat officiel « Quantum Bit », auteur : Focus on Frontier Technology
