Quand l'IA "résout" une conjecture sans preuve : la riposte des mathématiciens

Imaginez qu'un modèle d'IA annonce avoir résolu une conjecture géométrique vieille de quatre-vingts ans. Pas de preuve publiée dans une revue à comité de lecture, pas de code source disponible, pas de données d'entraînement communiquées. Juste un communiqué de presse. Pour un mathématicien, c'est à peu près aussi convaincant qu'un prestidigitateur qui prétend avoir découvert la loi de la gravité parce qu'il fait léviter un chapeau.

C'est précisément ce genre de situation — relatée par Ars Technica deux semaines après une annonce d'OpenAI sur un supposé résultat mathématique — qui a précipité la rédaction d'un texte collectif devenu, en quelques semaines, un événement dans la communauté internationale des mathématiques. La Leiden Declaration on Artificial Intelligence and Mathematics, déposée le 2 juin 2026 avec le DOI 10.5281/zenodo.20302944, n'est pas un règlement, pas une loi, pas un manifeste anti-technologie. C'est quelque chose de plus rare : un texte de normes, rédigé par des chercheurs pour des chercheurs, au moment précis où une discipline réalise que ses règles du jeu sont en train de changer sans qu'elle ait été consultée.

Tout commence en septembre 2025, lors d'un atelier au Lorentz Center de Leiden intitulé « Mechanization and Mathematical Research ». Environ soixante participants venus de dix pays — mathématiciens, informaticiens, historiens et anthropologues des sciences — se retrouvent pour discuter de ce que l'automatisation fait à leur discipline. De ces échanges naît un groupe de travail convoqué par Jim Portegies, de l'Eindhoven University of Technology, qui passe les six mois suivants à construire un texte commun, comme le raconte l'Université de Leiden.

Le résultat est signé par seize auteurs dont les affiliations couvrent Washington, Edinburgh, Amsterdam, Warwick, San Diego, Columbia, Cambridge, Oxford et Zurich. Rodrigo Ochigame, historien et anthropologue de l'IA à Leiden University et co-auteur, résume l'ambition : « Nous avons travaillé sur la déclaration pendant plusieurs mois, en rassemblant différents points de vue à la recherche de principes partagés. » Le texte a depuis reçu l'endossement de l'International Mathematical Union — l'organisation internationale associée notamment aux médailles Fields et au Congrès international des mathématiciens (ICM). Son secrétaire général, Christoph Sorger, a tenu à préciser : « L'IMU endosse la Déclaration de Leiden parce qu'elle constitue une contribution opportune, sérieuse et équilibrée à un débat qui ne fait que commencer. » Et d'ajouter : « Cet endossement ne signifie pas la fin du débat. »

Le texte identifie cinq valeurs fondamentales de la recherche mathématique que l'usage actuel de l'IA menace : la certitude des preuves, l'attribution vérifiable des résultats, la transparence des arguments, les standards collectifs d'évaluation, et l'autonomie de la discipline face aux logiques commerciales extérieures.

La première menace est peut-être la plus technique — et la plus sournoise. « Les techniques automatisées actuelles peuvent produire des arguments plausibles mais peu fiables, voire incorrects, difficiles à distinguer de vraies preuves mathématiques », avertit la déclaration. Vous voyez le problème : une preuve mathématique n'est pas un texte qui ressemble à une démonstration. C'est un objet logique dont chaque étape doit être vérifiable. Un grand modèle de langage peut enchaîner des symboles avec une fluidité impressionnante tout en commettant une erreur de raisonnement à la ligne 47 — erreur que seul un expert humain attentif détectera.

La distinction est fondamentale. Comme le formule Jeremy Avigad, professeur à Carnegie Mellon University, dans son article sur le tournant formel en mathématiques : « Nous pouvons maintenant écrire des définitions, des théorèmes et des preuves dans des langages idéalisés, semblables aux langages de programmation, que les ordinateurs peuvent interpréter et vérifier. » Mais vérifier n'est pas générer. Et c'est exactement là que les modèles d'IA générative posent problème : ils génèrent sans garantir.

La deuxième menace touche à l'attribution et au droit d'auteur. Des mathématiciens voient leurs articles publiés sur arXiv — librement accessibles, dans la tradition d'ouverture de la discipline — aspirés pour entraîner des modèles commerciaux, sans consentement et sans compensation. Ochigame le formule sans détour : « Des mathématiciens qui n'avaient jamais eu l'intention de contribuer au développement de l'IA voient leur travail utilisé à cette fin sans leur accord. »

La troisième menace, plus diffuse, est celle du hype — le battage médiatique. Michael Harris, mathématicien à Columbia University et co-auteur de la déclaration, pose le diagnostic avec une précision chirurgicale : « L'industrie technologique procède selon une logique commerciale, qui est antithétique aux valeurs des mathématiques. » Quand une entreprise annonce un résultat mathématique par communiqué de presse avant toute publication vérifiable, elle court-circuite le processus de validation collective qui est, depuis des siècles, le cœur de la pratique mathématique.

Derrière les enjeux éthiques se cache une question mathématique et informatique précise. Comment savoir qu'une preuve est juste si on ne peut pas la vérifier soi-même ? La communauté des assistants de preuve formels — des logiciels comme Lean ou Coq — a développé depuis les années 1970 une réponse élégante : le critère de de Bruijn. Comme l'expliquent Henk Barendregt et Freek Wiedijk dans leur article fondateur sur le défi des mathématiques computationnelles, un assistant de preuve satisfait ce critère si la démonstration produite peut être contrôlée indépendamment par un petit programme de vérification, séparé du système qui a aidé à la construire. La confiance ne repose pas sur l'intelligence du générateur, mais sur la transparence du vérificateur.

C'est exactement ce que les modèles d'IA propriétaires ne fournissent pas. Quand le modèle est inaccessible, comme le souligne Ochigame, « le modèle d'IA est propriétaire et indisponible pour quiconque en dehors de l'entreprise » — il n'y a pas de critère de de Bruijn possible. Pas de vérification indépendante. Pas de preuve au sens mathématique du terme.

La bibliothèque Mathlib, développée pour l'assistant de preuve Lean et décrite dans l'article de la communauté mathlib, illustre l'alternative : un corpus communautaire de définitions, théorèmes et preuves vérifiées, couvrant l'algèbre, la topologie, la théorie des catégories, l'analyse — construit de manière distribuée, sans autorité centrale, et librement consultable. C'est le modèle que la déclaration défend implicitement : ouvert, vérifiable, attribuable.

Les recommandations sont précises et opérationnelles. Les chercheurs sont invités à déclarer explicitement l'usage d'outils automatisés — grands modèles de langage, assistants de preuve, logiciels mathématiques — dans une section dédiée de leurs articles. La responsabilité de l'exactitude des résultats reste humaine. Les résultats ne doivent pas être présentés comme produits uniquement par une entreprise ou un modèle quand des contributions humaines et des travaux antérieurs sont impliqués. Et les auteurs doivent pouvoir refuser que leurs publications servent de données d'entraînement.

La déclaration ne demande pas d'interdire l'IA en mathématiques. Leslie Ann Goldberg, responsable de l'informatique à l'University of Oxford et co-signataire, formule le risque réel avec sobriété : « Les brouillons inexacts générés par IA sont bon marché à produire, et il existe un risque d'encombrer la littérature avec des résultats prétendus qui sont tout simplement faux. » Le problème n'est pas l'outil. C'est l'absence de normes pour l'utiliser.

Peter Scholze, directeur du Max Planck Institute for Mathematics et médaillé Fields, résume l'enjeu philosophique : « Le but de la recherche mathématique est la compréhension humaine des mathématiques, donc les mathématiques ne peuvent prospérer que dans une communauté de chercheurs humains. » La déclaration elle-même le formule en une phrase : « Les mathématiques sont, et doivent toujours rester, une entreprise profondément humaine. »

Une discussion dédiée est prévue le 26 juillet 2026 lors de l'ICM 2026, comme l'annonce l'IMU News de mai 2026. Le débat ne fait que commencer.

Pour comprendre précisément ce qui est en jeu, il faut distinguer trois niveaux de rapport entre l'IA et la preuve mathématique.

Le premier niveau est la génération de texte mathématique : un grand modèle de langage produit un texte qui ressemble à une démonstration, en langage naturel. C'est ce que font les modèles comme GPT-4 ou Claude. Le problème est que la plausibilité textuelle et la validité logique sont deux choses différentes. Un modèle peut halluciner une étape de raisonnement avec la même fluidité qu'il énonce un lemme correct.

Le deuxième niveau est la vérification formelle : une preuve est écrite dans un langage formel — Lean, Coq, Isabelle — que l'assistant de preuve peut contrôler mécaniquement. Comme l'ont montré Jeremy Avigad et John Harrison dans leur article publié dans Communications of the ACM, la vérification formelle pourrait devenir un nouveau standard de rigueur en mathématiques. Ici, la confiance ne repose pas sur l'expertise du lecteur mais sur la logique du vérificateur.

Le troisième niveau, le plus ambitieux, est l'autoformalisation : traduire automatiquement une preuve en langage naturel vers un objet formel vérifiable. Le benchmark ProofNet, présenté dans un article d'Azerbayev, Piotrowski, Schoelkopf, Ayers, Radev et Avigad, contient 371 exemples associant chacun un énoncé formel en Lean 3, un énoncé en langage naturel et une preuve en langage naturel, tirés de manuels de niveau universitaire en analyse réelle, algèbre linéaire et topologie. Résultat : dans leurs expériences, le modèle Code-davinci-002 formalisait correctement 13,4 % des théorèmes en mode few-shot (c'est-à-dire avec quelques exemples fournis en contexte) et 16,1 % avec récupération de prompts similaires. Le taux de vérification syntaxique (typecheck rate) atteignait 45,2 % avec récupération de prompts — ce qui signifie que plus de la moitié des sorties produites ne passaient même pas le contrôle syntaxique de Lean, avant toute question de validité mathématique.

Ces chiffres ne sont pas un réquisitoire contre l'IA en mathématiques. Ils montrent simplement que le chemin entre « texte mathématique convaincant » et « preuve formellement vérifiée » est encore long — et que la Leiden Declaration a raison de distinguer soigneusement les deux.