Une preuve produite par l'IA est-elle vraiment fiable ?

Des chercheurs de prestigieuses universités (Cambridge, Oxford, Columbia, ETH Zurich) ont publié la Déclaration de Leiden, un texte de onze pages soulevant des enjeux cruciaux pour la fiabilité mathématique à l'ère de l'IA. Le problème central : les systèmes d'IA produisent des arguments qui ressemblent formellement à des preuves mathématiques, mais sans garantie de correction et sans possibilité de vérification indépendante fiable par les pairs.

Le cas d'AlphaProof illustre cette préoccupation. Google DeepMind a annoncé en juillet 2024 la résolution de trois problèmes de l'Olympiade Internationale de Mathématiques, mais la méthodologie détaillée n'a été publiée que le 12 novembre 2025, plus d'un an après. Pendant ce délai, la communauté mathématique n'avait pas accès aux informations nécessaires pour évaluer la méthode globalement. Les signataires dénoncent également que les modèles d'IA exploitent massivement les publications mathématiques sans consentement explicite et ne citent souvent pas leurs sources, ce qui viole un principe fondamental : en mathématiques, citer les résultats antérieurs est inhérent à la démonstration elle-même. Sans ces citations, aucune vérification indépendante n'est possible.