Il existe une démonstration mathématique que personne, sur Terre, n’a jamais lue en entier. Personne. Et pourtant, nous la tenons pour vraie.
Depuis Euclide, les mathématiques reposent sur un pacte tacite entre les esprits. La démonstration est un acte de langage, bien davantage qu’un simple calcul. Elle s’adresse à quelqu’un. Elle progresse pas à pas, expose chaque étape, contraint la raison de celui qui suit à ne pouvoir qu’acquiescer. La vérité mathématique, contrairement à la foi ou à l’intuition, ne demande pas qu’on la croie : elle exige qu’on la voie.
Le contrat originel
Ce contrat est vieux de vingt-cinq siècles. Un pair compétent relit, vérifie, valide ou réfute. La communauté mathématique fonctionne comme une république des preuves : rien n’est vrai tant que personne n’a parcouru le chemin jusqu’au bout. La démonstration est à la fois l’argument et son propre garant, à condition qu’un esprit humain soit capable de la tenir tout entière en vue.
C’est précisément ce contrat qui est en train de se déchirer. Pour une raison plus ancienne que l’IA, plus profonde, que l’IA ne fait qu’aggraver.
La fracture silencieuse
La Classification des groupes simples finis est l’un des grands théorèmes du XXe siècle. Elle établit la liste complète des « atomes » de la symétrie algébrique. Sa démonstration a mobilisé plus d’une centaine de mathématiciens pendant plusieurs décennies. Elle occupe environ dix à quinze mille pages, réparties dans des centaines d’articles dispersés dans des revues spécialisées.
Aucun mathématicien ne possède une vision complète de cette démonstration.
Pourtant, la communauté mathématique tient ce théorème pour vrai. Elle y fait confiance, collectivement, partiellement, aveuglément en un sens. C’est une nouvelle forme de rationalité, où la vérification globale est distribuée entre des dizaines de spécialistes qui ne se sont jamais tous assis autour d’une même table.
La preuve de la conjecture de Kepler par Thomas Hales, en 1998, présentait un problème analogue : trois cents pages de démonstration, auxquelles s’ajoutait un code informatique de plusieurs gigaoctets. Les évaluateurs du journal Annals of Mathematics déclarèrent, après quatre ans de travail, être « sûrs à 99 % » de la validité de la preuve. Un pourcentage. Dans une discipline réputée pour ses certitudes absolues.
Avant même que les assistants de preuve formelle n’existent, le contrat originel était donc déjà rompu. La démonstration avait dépassé les capacités de vérification d’un cerveau humain. Ce que les nouvelles technologies révèlent, c’est une limite déjà inscrite dans la pratique des mathématiques.
La certification par la machine
Les assistants de preuve formelle (Lean, Coq) proposent une réponse à cette crise silencieuse. Ils permettent de traduire un raisonnement mathématique en langage informatique que la machine vérifie formellement, instruction par instruction, sans fatigue ni approximation. Une preuve certifiée par Lean est, en un sens technique précis, incontestable.
L’intelligence artificielle entre en scène différemment : elle peut explorer, suggérer des pistes, générer des hypothèses que les assistants de preuve valident ou rejettent. Terence Tao, médaille Fields et l’un des mathématiciens les plus importants de notre époque, a commencé à intégrer ces outils dans ses recherches, pour s’amplifier, pour aller plus loin que ce que l’esprit seul atteint.
Mais une question demeure, que la technique ne résout pas. La machine certifie. Elle garantit la forme du raisonnement. Elle ne comprend pas. Elle ne voit pas pourquoi. Elle ne saisit pas la beauté d’un argument, la surprise d’un détour inattendu, l’élégance d’une solution qui éclaire d’un seul coup ce que des approches frontales n’atteignaient pas. Elle produit une attestation. La compréhension reste hors de sa portée.
La question devient alors inévitable : qu’est-ce qu’une vérité que personne ne comprend ?
Une vérité sans témoin
Wittgenstein, dans ses Investigations philosophiques, posait une question apparemment technique mais aux implications profondes : peut-on suivre une règle seul ? Sa réponse, après un long détour, était qu’une règle n’a de sens que dans une pratique partagée, dans un usage social. Une règle que personne ne peut appliquer cesse d’être une règle : elle devient une forme vide.
Transposée aux mathématiques : une démonstration que personne ne peut parcourir est-elle encore une démonstration, ou seulement un objet mathématique dont nous postulons la validité ? Il y a une différence entre savoir qu’une chose est vraie et comprendre pourquoi elle l’est. La première relève de la certification. La seconde relève de la connaissance.
Gödel avait déjà révélé cette tension depuis un autre angle. Ses théorèmes d’incomplétude montrent que la vérité mathématique déborde toujours les systèmes formels qui prétendent la capturer entièrement. Il existe des énoncés vrais qu’aucun système ne peut démontrer depuis l’intérieur. La vérité dépasse la démontrabilité. Elle dépasse désormais aussi la compréhensibilité.
G. H. Hardy, dans son Apologie d’un mathématicien, défendait une thèse qui peut sembler naïve mais qui mérite attention : la beauté d’une démonstration est un signal, avant d’être un ornement. Quand une preuve est élégante, c’est que l’esprit a saisi une structure, une nécessité, une vérité qui se révèle dans sa propre lumière. La beauté est le signe de la compréhension.
Une démonstration de quinze mille pages vérifiée par une machine est-elle encore belle ? Peut-elle l’être ? Et si elle ne l’est pas, qu’avons-nous perdu, au-delà de la vérification ?
Dans la tradition juridique, on distingue le fait établi du fait compris. Un verdict peut être prononcé sans que la vérité soit vraiment atteinte. La justice a besoin de témoins autant que de preuves. Les mathématiques ont toujours fonctionné du côté du témoignage : la démonstration est adressée à quelqu’un. Retirer le témoin, c’est peut-être changer la nature même de ce qu’on appelle vérité en mathématiques.
Ce que la machine ne peut pas remplacer
Il serait trop facile de conclure sur une nostalgie. Les mathématiques ne mourront pas de leur propre complexité. Elles se transforment, comme elles se sont toujours transformées.
Cette transformation pose une question philosophique. Terence Tao se sert des assistants de preuve pour aller plus loin dans ce que l’esprit humain fait de mieux : chercher, intuitionner, relier, s’émerveiller. La machine vérifie. L’humain questionne. Et poser une bonne question demeure hors de portée de tout algorithme.
La vraie rupture se situe ailleurs : dans la complexité croissante d’une discipline qui a atteint des régions où l’esprit humain ne peut plus voyager seul. Les outils formels constituent une réponse à cette situation : nécessaire, partielle, porteuse de nouvelles questions.
Ces outils dessinent les contours d’un nouveau rapport au savoir : la certification collective prend la place que la compréhension individuelle occupait. Ce glissement est discret. Il est profond.
La question centrale est autre : que devient une discipline dont les vérités les plus profondes ne sont plus accessibles à l’esprit qui les a cherchées ?
La vraie question
Revenons au contrat originel. La démonstration était un acte de communication entre des esprits. Elle s’adressait à quelqu’un. Elle présupposait un lecteur capable de la suivre, de s’y perdre, d’y revenir, de la comprendre enfin.
Ce lecteur est en train de disparaître, parce que certaines vérités ont grandi au-delà de ce qu’un esprit peut embrasser, quelle que soit sa rigueur. Le savoir continue de croître alors même que la compréhension individuelle atteint ses limites. C’est la tension propre à notre époque.
Lean certifie. Coq valide. L’IA explore. Mais aucun de ces outils ne peut répondre à la question la plus ancienne des mathématiques : pourquoi ce théorème est-il beau ? Pourquoi cette démonstration éclaire-t-elle un horizon qui la dépasse elle-même ?
La vraie question est presque antique : une vérité existe-t-elle encore si personne ne peut la parcourir ?
Euclide aurait peut-être répondu que non. La vérité mathématique a toujours été un acte de partage, une traversée commune. Retirer le compagnon de route, c’est peut-être changer la nature du voyage.
Nous n’avons pas encore mesuré ce que cela signifie.
Didier Aubourg (*)
(*) Didier Aubourg est ingénieur, écrivain et poète. Il anime l’émission littéraire Passeurs & Rêveurs des mots sur Radio Top Side et a cofondé l’association Les Plumes des Rivieras. Son recueil de poésie « Ce que l’Univers murmure » est paru en 2026 aux éditions Les Bonnes Feuilles.