IA et preuves mathématiques : la crise de confiance

Résumé exécutif

• Un groupe de mathématiciens de Cambridge, Oxford, Columbia et ETH Zurich a publié un texte de onze pages sur les risques que l’IA fait peser sur leur discipline.
• Les systèmes d’IA peuvent produire des arguments qui ressemblent à des preuves mathématiques sans que leur exactitude puisse être vérifiée sans un travail considérable.
• Les techniques automatisées actuelles génèrent des pseudo-preuves difficiles à distinguer de vraies preuves.
• Google DeepMind a annoncé AlphaProof en juillet 2024, avant toute vérification scientifique indépendante ; la publication dans Nature n’a eu lieu que plus d’un an après.
• La Déclaration de Leiden dénonce cette pratique d’annonces commerciales prépubliées et demande aux entreprises de ne pas exploiter les publications mathématiques sans consentement explicite des auteurs.
• Les modèles entraînés sur des publications mathématiques omettent fréquemment de citer les travaux humains, rendant impossible la vérification indépendante des raisonnements.

Introduction

La rigueur mathématique repose sur un principe fondamental : toute preuve publiée doit pouvoir être vérifiée de manière indépendante par n’importe quel pair compétent. Ce processus garantit la fiabilité de la connaissance mathématique et permet aux chercheurs de bâtir sur des fondations solides. Or, l’émergence de modèles d’intelligence artificielle capables de générer des chaînes de raisonnement formelles remet en question cette confiance.

Un système d’IA peut produire un argument qui imite la structure d’une preuve mathématique sans que personne ne puisse en garantir la correction sans un travail de vérification exhaustif. Cette capacité à créer des « pseudo-preuves » soulève une menace sérieuse pour l’intégrité de la discipline. Des chercheurs de Cambridge, Oxford, Columbia et de l’ETH Zurich ont publié un texte collectif de onze pages qui expose les risques concrets et propose des remèdes, notamment à travers la Déclaration de Leiden. Cet article détaille les problèmes posés par les preuves générées par IA, analyse le cas emblématique d’AlphaProof de Google DeepMind, et examine les enjeux de citation et de transparence dans la recherche mathématique.

La menace des preuves illusoires

Une preuve mathématique classique suit des règles logiques strictes et chaque étape peut être vérifiée par un humain. Lorsqu’un mathématicien publie une démonstration, n’importe lequel de ses pairs peut la reproduire et en confirmer la validité. Avec les systèmes d’IA, cette garantie disparaît. Les modèles entraînés sur de vastes corpus mathématiques génèrent des enchaînements d’affirmations qui semblent plausibles mais dont la correction n’est pas assurée.

Le problème ne vient pas uniquement d’erreurs accidentelles. Les techniques automatisées actuelles produisent délibérément des « preuves » qui ressemblent à des démonstrations authentiques, mais qui peuvent contenir des sauts logiques, des hypothèses implicites ou des conclusions fausses. Ces artefacts sont difficiles à distinguer de vraies preuves, même pour des experts. La vérification manuelle d’une pseudo-preuve peut exiger des semaines de travail, annulant l’avantage supposé de rapidité apporté par l’IA.

Les signataires du texte mettent en garde contre le risque que ces résultats trompeurs encombrent la littérature mathématique. Une fois publiée, une pseudo-preuve peut être reprise par d’autres travaux, qui s’y appuient pour construire de nouvelles démonstrations. L’erreur se propage alors comme une traînée de poudre, contaminant des branches entières de la recherche. La correction de ces erreurs ultérieures devient d’autant plus difficile que les modèles d’IA ne fournissent pas de traçabilité claire de leurs sources.

AlphaProof : un précédent inquiétant

Le 24 juillet 2024, Google DeepMind a annoncé par communiqué de presse qu’AlphaProof, un système d’IA dédié aux mathématiques, avait atteint le niveau d’une médaille d’argent aux Olympiades internationales de mathématiques. L’annonce a été relayée par de nombreux médias avant que la communauté scientifique n’ait eu accès aux détails de la méthode. La publication officielle dans la revue Nature n’a eu lieu que le 12 novembre 2025, soit plus d’un an après.

Pendant cette période, les mathématiciens n’ont pas pu évaluer la validité de l’approche. Deux chercheurs, Tim Gowers et Joseph Myers, avaient bien vérifié les solutions soumises lors de la compétition, mais cette vérification ponctuelle ne suffit pas à juger une méthode dans son ensemble. Un système d’IA peut produire des solutions correctes pour quelques problèmes tout en restant peu fiable sur d’autres classes de questions. Sans accès aux données d’entraînement, aux hyperparamètres et aux évaluations systématiques, il est impossible de déterminer la robustesse d’AlphaProof.

Ce cas illustre un problème plus large, dénoncé par la Déclaration de Leiden. Cette déclaration, élaborée lors d’un atelier en septembre 2025 au Lorentz Center de Leiden par un groupe de travail de dix-sept membres, critique la pratique qui consiste à annoncer des résultats sur des délais commerciaux, avant que la communauté scientifique puisse se prononcer. Selon Leslie Ann Goldberg, responsable du département d’informatique à Oxford, cette habitude touche l’ensemble du secteur de l’IA, pas seulement Google DeepMind.

L’enjeu des citations et de la propriété intellectuelle

En mathématiques, citer les résultats antérieurs sur lesquels un raisonnement s’appuie n’est pas une formalité bibliographique : cela fait partie intégrante de la démonstration. Un raisonnement qui repose sur un résultat non identifié ne peut pas être vérifié de façon indépendante, car on ignore si ce résultat est lui-même correct.

Or, les modèles d’IA entraînés sur des publications mathématiques retournent fréquemment des résultats sans citer les travaux humains qu’ils agrègent. Beaucoup de ces modèles ont été construits à partir de données obtenues en exploitant des licences et des accords d’accès qui n’avaient pas été prévus pour l’entraînement d’IA, parfois en violant des restrictions d’accès.

L’absence de citation crée une double dépendance : le mathématicien qui utilise une IA ne peut remonter aux sources, et la vérification devient impossible. De plus, cela fragilise la reconnaissance des auteurs humains, déjà confrontés à une pression croissante dans l’évaluation de leurs travaux. Leslie Ann Goldberg souligne que la recherche mathématique se construit presque toujours sur des travaux antérieurs, et que des brouillons générés par IA risquent d’encombrer la littérature de résultats annoncés corrects mais faux.

Les revendications des mathématiciens

Face à ces menaces, les signataires de la Déclaration de Leiden formulent plusieurs demandes précises. Ils exigent des entreprises technologiques qu’elles n’utilisent pas des publications mathématiques comme données d’entraînement sans le consentement explicite de leurs auteurs. Ils réclament également une transparence totale sur les données utilisées et les méthodes de vérification employées.

La déclaration reste ouverte aux signatures de la communauté mathématique, et ses auteurs espèrent qu’elle servira de base à des normes internationales. Le texte insiste sur le fait que la pratique actuelle, qui combine annonces prématurées et absence de traçabilité, menace la confiance dans l’ensemble de l’édifice mathématique. Sans une régulation claire, les pseudo-preuves risquent de se multiplier, rendant la littérature mathématique de moins en moins fiable.

À retenir

1. Les systèmes d’IA peuvent générer des arguments qui imitent des preuves mathématiques sans en garantir l’exactitude, ce qui rend leur vérification extrêmement coûteuse.
2. Google DeepMind a annoncé AlphaProof avant toute validation indépendante, un cas de non-respect des normes académiques que la Déclaration de Leiden condamne.
3. L’absence de citation des travaux humains par les modèles d’IA empêche la vérification indépendante des raisonnements.
4. Les erreurs introduites par des pseudo-preuves risquent de se propager dans la littérature mathématique, contaminant les recherches futures.
5. Les mathématiciens demandent le consentement explicite des auteurs pour utiliser leurs publications comme données d’entraînement.
6. La Déclaration de Leiden, développée sur huit mois par un groupe de travail de dix-sept membres, propose un cadre pour restaurer la confiance.

Questions fréquentes

Qu’est-ce qu’une pseudo-preuve mathématique générée par IA ?

C’est une chaîne de raisonnement produite par un modèle d’IA qui a la forme d’une démonstration mathématique (déductions, symboles, références) mais dont la correction logique n’est pas garantie. Contrairement à une preuve humaine, aucun pair n’a vérifié sa validité de manière indépendante, et l’IA ne fournit pas les étapes intermédiaires nécessaires à une telle vérification.

Pourquoi le cas AlphaProof est-il critiqué par les mathématiciens ?

AlphaProof a été annoncé par Google DeepMind en juillet 2024 avant qu’une publication scientifique évaluée par les pairs ne paraisse. Pendant plus d’un an, la communauté n’a pas eu accès aux détails de la méthode, ce qui a empêché une évaluation indépendante du système. La vérification de solutions ponctuelles par deux experts ne remplace pas une analyse de la robustesse globale.

Que demande la Déclaration de Leiden ?

La déclaration, élaborée par des mathématiciens de plusieurs grandes universités, demande aux entreprises de ne pas utiliser des publications mathématiques pour entraîner des IA sans le consentement explicite des auteurs. Elle exige également une transparence sur les données d’entraînement et les méthodes de vérification, afin de garantir que les résultats produits par IA puissent être contrôlés.

Conclusion

L’intelligence artificielle offre des perspectives fascinantes pour la découverte mathématique, mais elle introduit en même temps un risque fondamental : la perte de confiance dans la fiabilité des preuves. La capacité des systèmes à générer des pseudo-preuves indiscernables de démonstrations authentiques met en péril le processus même qui garantit la rigueur de la discipline. Le cas AlphaProof illustre comment des annonces commerciales prématurées peuvent court-circuiter l’évaluation scientifique, tandis que l’absence de citation des travaux humains sape les fondements de la vérification.

La Déclaration de Leiden constitue une première tentative pour poser des garde-fous. Mais son efficacité dépendra de l’engagement des entreprises technologiques et de la communauté mathématique dans son ensemble. À mesure que les modèles d’IA deviendront plus performants, la frontière entre preuve authentique et illusion algorithmique deviendra encore plus ténue. La seule réponse durable consiste à exiger la transparence, le consentement et une vérification indépendante systématique, sans quoi les mathématiques risquent de perdre leur statut de science exacte.