Une démonstration de 500 pages que personne n'a pu lire jusqu'au bout
Imaginez qu'un mathématicien publie, du jour au lendemain, une démonstration de l'un des problèmes les plus difficiles de son domaine — et que, douze ans plus tard, personne ne soit encore capable de dire si elle est juste ou fausse. C'est exactement ce qui se passe depuis 2012 avec la conjecture abc, et c'est peut-être le plus grand scandale silencieux de l'histoire des mathématiques modernes. Pour en finir, des chercheurs ont décidé de confier le verdict à une machine.
La conjecture abc : un problème d'apparence simple, d'une profondeur abyssale
Avant d'entrer dans le vif du sujet, posons les bases. La conjecture abc est un énoncé sur les nombres entiers, formulé dans les années 1980 par les mathématiciens Joseph Oesterlé et David Masser. Son idée centrale peut se résumer ainsi : si trois entiers a, b et c vérifient l'équation a + b = c, alors les facteurs premiers qui composent ces trois nombres ne peuvent pas être tous très petits à la fois. Autrement dit, une somme simple entre deux entiers contraint la structure profonde de leurs diviseurs.
Cette conjecture peut sembler anodine formulée ainsi, mais ses implications sont considérables : si elle était prouvée, elle entraînerait automatiquement la démonstration de dizaines d'autres théorèmes importants en théorie des nombres — la branche des mathématiques qui étudie les propriétés des entiers. Le dernier théorème de Fermat, par exemple, en découlerait presque comme un corollaire. La conjecture abc est donc une sorte de clé de voûte : la valider, c'est ouvrir des dizaines de portes d'un seul coup.
Mochizuki, le solitaire de Kyoto
En août 2012, Shinichi Mochizuki, professeur à l'université de Kyoto, publie sur son site personnel quatre articles totalisant plus de 500 pages. Il y annonce avoir démontré la conjecture abc. Mais la démonstration ne ressemble à rien de connu : elle s'appuie sur une théorie entièrement nouvelle, que Mochizuki a développée seul pendant une décennie et qu'il appelle la théorie des espaces de Teichmüller inter-universels — ou IUT pour les intimes.
Le problème ? Cette théorie invente ses propres objets mathématiques, ses propres notations, ses propres règles du jeu. Pour comprendre la preuve, il faut d'abord apprendre un langage que personne d'autre n'a jamais parlé. Des mathématiciens parmi les plus brillants du monde ont essayé. Beaucoup ont abandonné après des semaines ou des mois d'effort. Peter Scholze et Jakob Stix, deux géants de la théorie des nombres, ont finalement affirmé en 2018 avoir identifié une faille précise dans l'argumentation — une étape clé du raisonnement qui, selon eux, ne tient pas.
« Nous ne comprenons pas pourquoi cette étape est supposée fonctionner, et nous ne croyons pas qu'elle fonctionne. » — Peter Scholze et Jakob Stix, 2018
—
Mochizuki, de son côté, a maintenu que ses critiques n'avaient tout simplement pas compris sa théorie. Il a répondu longuement, point par point, sans jamais concéder la moindre erreur. Et là, le dialogue s'est arrêté. Deux camps se sont formés : ceux qui pensent que la preuve est correcte (principalement des proches collaborateurs de Mochizuki au Japon), et ceux qui estiment qu'elle est trouée. Le reste de la communauté, la grande majorité, a simplement renoncé à trancher.
Pourquoi une preuve peut rester indécidable pendant dix ans
Ce cas illustre une limite profonde du système de validation des mathématiques. En principe, une démonstration mathématique est soit correcte, soit incorrecte — il n'y a pas de zone grise. Mais en pratique, la validation repose sur la peer review, c'est-à-dire la relecture par des pairs : d'autres experts du domaine qui vérifient chaque étape du raisonnement. Ce système fonctionne très bien quand une preuve s'inscrit dans un langage partagé. Il s'effondre quand la preuve réinvente ce langage de toutes pièces.
Personne n'est payé pour passer six mois à apprendre une théorie entière juste pour vérifier si elle est cohérente. Les mathématiciens ont des cours à donner, des articles à publier, des carrières à construire. Auditer la preuve de Mochizuki représente un investissement colossal pour un retour incertain. Résultat : la preuve a bien été publiée dans un journal — les Publications of the Research Institute for Mathematical Sciences de Kyoto, dont Mochizuki est lui-même l'éditeur en chef, ce qui a suscité des critiques sur les conflits d'intérêts — mais sans jamais obtenir la validation informelle de la communauté internationale.
L'ordinateur comme arbitre de dernier recours
C'est dans ce contexte de blocage total qu'une nouvelle approche émerge : la vérification formelle assistée par ordinateur. Le principe est le suivant. Des logiciels spécialisés — appelés proof assistants, ou assistants de preuve — permettent de traduire une démonstration mathématique en un langage formel que la machine peut vérifier étape par étape, mécaniquement, sans fatigue ni biais. Si une étape ne tient pas, l'ordinateur le détecte.
Des chercheurs ont entrepris de formaliser des parties clés de la théorie IUT dans l'un de ces assistants. L'objectif est précis : vérifier l'étape exacte que Scholze et Stix ont mise en cause. Si l'ordinateur confirme la faille, le débat est clos. Si, au contraire, il valide l'étape, cela obligera la communauté à reconsidérer ses objections.
Ce n'est pas une démarche triviale. Formaliser des mathématiques avancées dans un assistant de preuve demande un travail considérable — parfois des années pour quelques pages. Mais c'est peut-être le seul moyen de sortir d'une impasse que les humains seuls n'ont pas réussi à résoudre.
Les leçons d'un scandale mathématique
Au-delà du cas Mochizuki, cette affaire pose des questions qui dépassent largement un seul homme ou une seule conjecture. Comment la communauté mathématique doit-elle traiter les théories radicalement nouvelles, celles qui demandent des années d'apprentissage avant même de pouvoir être évaluées ? Qui doit supporter le coût de la vérification ? Et si personne ne le fait, une preuve non lue est-elle vraiment une preuve ?
L'essor des assistants de preuve ouvre une piste sérieuse. Des mathématiques formalisées sont vérifiables par n'importe qui disposant du logiciel adéquat. Elles ne dépendent plus de la bonne volonté d'une poignée d'experts surchargés. Certains chercheurs militent déjà pour que les grandes preuves soient systématiquement accompagnées de leur version formelle. Ce serait une révolution dans la façon dont les mathématiques se font et se transmettent.
En attendant, le verdict de la machine est attendu avec une impatience teintée d'inquiétude. Car si l'ordinateur confirme la faille, il faudra tirer une conclusion inconfortable : pendant plus d'une décennie, la communauté mathématique mondiale a été incapable de valider ou d'invalider l'un de ses propres résultats supposés majeurs. Et ça, c'est une faille dans le système, pas seulement dans une preuve.
Concepts à emporter
Pour les matheux
La conjecture abc se formule précisément à l'aide de la notion de radical d'un entier. Pour un entier n, on définit rad(n) comme le produit de tous les facteurs premiers distincts de n — sans tenir compte de leurs multiplicités. Par exemple, rad(12) = rad(2² × 3) = 2 × 3 = 6. La conjecture stipule alors que pour tout réel ε > 0, il n'existe qu'un nombre fini de triplets d'entiers (a, b, c) premiers entre eux deux à deux, vérifiant a + b = c, et tels que c > rad(abc)1+ε. Autrement dit, les cas où c est « beaucoup plus grand » que le radical du produit abc sont extrêmement rares. Cette formulation capture l'idée que les puissances élevées dans les facteurs premiers d'une somme sont une anomalie, pas la norme.
