En mathématiques, la longueur d'une démonstration dépend du langage (naturel ou formel) dans lequel elle est rédigée, ainsi que des résultats préliminaires sur lesquels elle s'appuie. Des résultats inattendus de la théorie de la démonstration, comme le théorème d'accélération de Gödel, montrent que des énoncés simples peuvent avoir des démonstrations très longues, et qui dépendent considérablement du système d'axiomes choisis ; si les mathématiciens ont une préférence pour les « démonstrations élégantes » (qui sont souvent les plus courtes possibles), dans la seconde moitié du XX^e siècle, certaines résultats importants ont néanmoins fait l'objet de démonstrations, parfois assistées par ordinateur, d'une longueur exceptionnelle.

La rédaction des démonstrations mathématiques est nécessairement un compromis entre une rigueur parfaite (et le plus souvent inaccessible), mais illisible pour un lecteur humain, car se perdant dans trop de détails, et un style trop allusif, comportant des lacunes de raisonnement qui peuvent aller jusqu'à mettre en péril la justesse des résultats^{[N 1]}. Toutefois, sans sacrifier à la rigueur, les mathématiciens contemporains attachent une grande importance à ce qu'ils appellent l'élégance des démonstrations, qui se traduit souvent par la recherche de preuves courtes^{[N 2]}.

La recherche de la démonstration la plus courte (qui, contrairement par exemple à celle du programme le plus court exécutant une tâche donnée, est théoriquement toujours faisable pour un théorème démontré^{[N 3]}) s'avère en pratique d'une difficulté redoutable ; avec un critère légèrement différent, Paul Erdős a expliqué que ces démonstrations étaient « celles qui figuraient dans le livre de mathématiques de Dieu »^[1]. Le domaine de la complexité des preuves établit des résultats sur les tailles minimales des démonstrations selon divers systèmes de preuves^[2].

La conséquence de cette quête de la perfection est la diminution de la longueur de certaines démonstrations (souvent liée à l'apparition de résultats ou de méthodes plus puissants et plus généraux) ; cependant, la longueur moyenne des démonstrations a tendance à augmenter avec le temps, et si, par exemple, un article de théorie des groupes d'une vingtaine de pages était considéré comme long au début du XX^e siècle, des articles de plusieurs centaines de pages ont été publiés dans le cadre de l'étude des groupes finis à partir de 1960 ; d'ailleurs, en 2014, la plus longue démonstration recensée, mesurée par le nombre de pages publiées dans des revues mathématiques, est la classification des groupes finis simples, avec plus de dix mille pages. Toutefois, plusieurs démonstrations dépasseraient de loin ce record si les détails des calculs informatiques les justifiant étaient intégralement publiés ; les résultats de logique mathématique exposés ci-dessous amènent également à relativiser cette mesure.

L'idée de l'utilisation d'un langage formel pour la rédaction de démonstrations mathématiques nait, à la fin du XIX^e siècle, des besoins de la logique mathématique, et en particulier du désir d'automatiser les raisonnements ; on a souvent fait remarquer l'espace démesuré que prennent dans ces systèmes les démonstrations les plus simples, par exemple le fait qu'il faut plus de 300 pages à Russell et Whitehead pour démontrer rigoureusement que 1+1=2 dans les Principia Mathematica^{[N 4]}, ou le fait que l'écriture développée (sans abréviations) du nombre 1 dans le système de Nicolas Bourbaki demanderait des milliards de symboles^[3]. Cependant, en utilisant un système convenable d'abréviations, il est possible de formaliser complètement des textes mathématiques non triviaux, ce qui permet par exemple à des logiciels de vérification de preuves tels que Coq de contrôler rigoureusement leur exactitude^{[4],[N 5]}.

En 1936, Kurt Gödel, en adaptant sa démonstration du premier théorème d'incomplétude, a construit des exemples explicites d'assertions relativement courtes, démontrables dans un système formel donné, mais dont la plus courte démonstration dans ce système est absurdement longue^[5]. Ainsi, l'affirmation :

« Cette affirmation ne peut être prouvée à l'aide des axiomes de Peano (seuls) en moins d'un gogolplex de symboles »

(ou plus précisément, l'affirmation G qui code, au moyen d'un code de Gödel convenable, que G n'est pas démontrable en moins de N symboles) est effectivement vraie, et même démontrable dans PA (l'arithmétique de Peano) ; de plus, si PA est non-contradictoire, la démonstration possède nécessairement plus de N symboles. En revanche, il suffit d'adjoindre aux axiomes de Peano l'affirmation que ceux-ci sont non contradictoires (plus techniquement, l'axiome coh_PA, lequel, d'après le second théorème d'incomplétude, ne peut être démontré dans PA), pour pouvoir démontrer G en peu de symboles.

Par la suite, des exemples plus naturels du même phénomène ont été en particulier construits par Harvey Friedman, en utilisant des résultats de théorie des graphes tels que le théorème de Kruskal ou le théorème de Robertson-Seymour^[6].

Dans le même article, Gödel montrait également que la longueur (en fonction de n) des plus courtes démonstrations de certains théorèmes de longueur n croissait plus vite que toute fonction calculable de n, à l'aide d'un raisonnement très simple^{[N 6]} ; une analyse plus précise de ce résultat, utilisant la fonction du castor affairé, a été donnée par Gustavo Lacerda en 2014^[7].

Certaines démonstrations importantes de l'histoire des mathématiques tiennent en quelques dizaines de caractères, et les articles dans lesquels elles ont été publiées en une dizaine de lignes^{[8],[N 7]}. Notamment :

• la conjecture d'Euler, énoncée en 1772, n'a été réfutée qu'en 1966^[9], la démonstration se résumant à l'énoncé d'un contre-exemple^{[N 8]} : 27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵ ;

• la conjecture de Simpson concernant les systèmes couvrants, énoncée en 1987^[10], a de même été réfutée en 1989^[11] par le simple énoncé : D = {6, 15, 35, 14, 210 (140)}.

Ces deux démonstrations sont considérées comme complètes parce que l'égalité énoncée peut être vérifiée par un calcul arithmétique élémentaire. Elles diffèrent cependant en ce que la première peut être vérifiée très rapidement (en quelques secondes avec une calculette) alors que la seconde requiert qu'on comprenne la conjecture et implique un calcul extrêmement long, quoique élémentaire^[8].

La liste suivante (non exhaustive) est presque entièrement constituée de publications, faites après 1950, de résultats jugés importants par la communauté mathématique (et ayant souvent reçu des récompenses prestigieuses), dont la longueur inhabituelle a également fait l'objet de commentaires, en particulier concernant la difficulté de leur vérification. Dans plusieurs cas récents, comme les différents résultats liés à la classification des groupes finis simples, la démonstration proprement dite s'accompagne de calculs informatiques (voir la section suivante) qui, s'ils étaient intégralement publiés, augmenteraient, parfois énormément, les longueurs mentionnées ici.

• 1799 : Le théorème d'Abel-Ruffini fut presque démontré par Paolo Ruffini, mais sa démonstration, un livre de 500 pages^[12], fut pour l'essentiel ignorée ; en 1824, Niels Henrik Abel publia une démonstration ne comportant que six pages^[13].
• 1890 : La classification par Wilhelm Killing des algèbres de Lie simples (y compris sa découverte des algèbres exceptionnelles), occupe 180 pages en 4 articles^[14].
• 1894 : La construction du polygone régulier à 65 537 côtés par Johann Gustav Hermes (en) occupe plus de 200 pages^[15].
• 1905 : La démonstration initiale par Emanuel Lasker du théorème de décomposition primaire prenait 97 pages ; on peut à présent le démontrer en moins d'une page^[16].
• 1963 : La démonstration du théorème de l'ordre impair par Feit et Thompson prend 255 pages^[17] (mais a été substantiellement simplifiée depuis par Gonthier et son équipe pour pouvoir mener à bien leur démonstration certifiée par ordinateur^[18]) ; à cette époque, 25 pages est encore considéré comme long pour un article de théorie des groupes^{[réf. souhaitée]}.
• 1964 : Heisuke Hironaka démontre en 216 pages que toutes les singularités des variétés algébriques (de caractéristique nulle) sont résolubles (en) (cette démonstration a été simplifiée depuis jusqu'à une vingtaine de pages)^[19].
• 1966 : La démonstration par Abhyankar du même résultat pour les variétés de dimension 3 et de caractéristique > 6 est répartie en plusieurs articles, couvrant environ 500 pages^[20] (en 2009, Cutkosky la simplifie pour la ramener à 40 pages^[21]).
• 1966 : La construction par Harish-Chandra des représentations par séries discrètes des groupes de Lie est faite dans une longue suite d'articles totalisant environ 500 pages ; son prolongement par l'étude du théorème de Plancherel pour les groupes semi-simples occupe 150 pages supplémentaires^[22].
• 1968 : Piotr Novikov et Sergueï Adian montrent que la version bornée du problème de Burnside n'admet pas de solution. Leur article, paraissant en trois parties, fait plus de 300 pages^[23].
• 1960 à 1970 : Alexandre Grothendieck publie Fondements de la géométrie algébrique (FGA, plus de 1 000 pages), Éléments de géométrie algébrique (EGA, 1 500 pages) et les notes du Séminaire de géométrie algébrique ; ce travail de refondation de la géométrie algébrique contient certains théorèmes dont la démonstration repose sur plusieurs centaines de pages de résultats préliminaires, utilisés également dans le travail de Pierre Deligne en 1974^{[N 9]}.
• 1974 : Thompson achève la classification des N-groupes simples (en) dans une série de 6 articles totalisant environ 400 pages, et s'appuyant également sur le théorème de l'ordre impair, ce qui porterait la longueur totale à plus de 700 pages^[24].
• 1974 : La démonstration des conjectures de Weil (et d'une de leurs conséquences, la conjecture de Ramanujan) par Pierre Deligne ne fait « que » 30 pages^[25], mais elle repose sur un ensemble de résultats de géométrie algébrique et de cohomologie étale dont la longueur est estimée par Don Zagier à environ 2 000 pages^[26].
• 1974 : La démonstration d'Appel et Haken du théorème des quatre couleurs prend 139 pages^[27], mais c'est sans compter de longs calculs sur ordinateur (voir à ce sujet la section suivante).
• 1974 : Le théorème de Gorenstein-Harada (en) (un autre résultat partiel dont dépend le théorème de classification des groupes finis simples) occupe 464 pages^[28].
• 1976 : La construction par Robert Langlands de l'équation fonctionnelle des séries d'Eisenstein occupe 337 pages^[29].
• 1983 : Gorenstein et Lyons démontrent le théorème de trichotomie (en) dans le cas d'un rang > 3 dans un article de 731 pages^[30] ; la démonstration par Aschbacher du cas du rang 3 occupe 159 pages supplémentaires^[31].
• 1983 : La démonstration par Dennis Hejhal d'une généralisation de la formule des traces de Selberg occupe 2 volumes d'un total de 1 322 pages^[32],[33].
• 1974-2003 : Les démonstrations par James Arthur de différentes variantes de cette formule (en) occupent plusieurs centaines de pages dans de nombreux articles^[34].
• 1995 : La démonstration par Andrew Wiles du dernier théorème de Fermat ne comporte « que » 108 pages^[35], mais s'appuie sur un énorme corpus de résultats préliminaires^{[N 10]}.
• 2000 : La démonstration par Almgren de son théorème de régularité (en) occupe 955 pages^[36].
• 2000 : La démonstration par Laurent Lafforgue de la conjecture de Langlands pour le groupe linéaire (en) sur les corps de fonctions prend environ 600 pages, sans compter un volume bien plus important de résultats préliminaires^[37].
• 2003 : Les démonstrations de Grigori Perelman de la conjecture de Poincaré et de la conjecture de géométrisation ne sont pas très longues, mais ne sont que des esquisses ; des démonstrations complètes, publiées par la suite par d'autres mathématiciens, prennent plusieurs centaines de pages^{[N 11]}.
• 2004 : La classification des groupes quasi-fins (en) par Michael Aschbacher et Stephen Smith prend 1 221 pages ; c'est l'un des plus longs articles jamais écrit ; un second article presque aussi long démontre de nombreux théorèmes de structure à leur sujet^[38],[39]. Ces deux articles veulent mettre un point final à la classification des groupes finis simples.
• 2004 : Classification des groupes finis simples. La démonstration de ce théorème (et en particulier la détermination de la liste des 26 groupes sporadiques) était censée être achevée en 1983 ; cette démonstration était à l'époque dispersée dans plusieurs centaines d'articles de journaux, rendant difficile d'en estimer la longueur totale, sans doute comprise entre dix et vingt mille pages^[40]. Cependant, la vérification de cet ensemble, presque humainement impossible, a amené à en réécrire une partie sous forme de théorèmes plus puissants, en particulier ceux de Michael Aschbacher mentionnés précédemment.
• 2004 : Le théorème de Robertson-Seymour a une démonstration de 500 pages, occupant 20 articles publiés au long de deux décennies^{[N 12]}.
• 2006 : La démonstration du théorème des graphes parfaits, par Maria Chudnovsky, Neil Robertson, Paul Seymour, et Robin Thomas, prend 180 pages des Annals of Mathematics^[41].
• 2009 : La démonstration par Thomas Hales de la conjecture de Kepler, outre plusieurs centaines de pages de texte, s'accompagne de plusieurs gigaoctets de calculs informatiques^{[N 13]}.

Il n'y a pas vraiment de séparation nette entre calculs informatiques et démonstrations ; en un certain sens, tout calcul est d'ailleurs la démonstration d'un théorème : celui affirmant que le résultat de ce calcul est bien la valeur énoncée^[42]. Certaines des longues démonstrations mentionnées précédemment, comme celles du théorème des quatre couleurs ou de la conjecture de Kepler, utilisent de nombreuses pages de raisonnements mathématiques combinés à de longs calculs. Dans cette section-ci, les démonstrations proprement dites sont courtes, voire triviales, et les calculs sont, d'un point de vue mathématique, de pure routine (même si des techniques informatiques sophistiquées, comme le calcul distribué, ont parfois été utilisées pour les exécuter). Les quelques exemples typiques qui suivent sont souvent les derniers résultats (en 2022) d'une série de calculs analogues moins poussés, ayant parfois (comme pour celui des décimales de π) commencé dès l'aube de l'informatique^{[N 14]}.

• Plusieurs démonstrations de l'existence de certains groupes sporadiques, comme le groupe de Lyons, se sont d'abord appuyées sur des calculs mettant en jeu de grandes matrices ou des permutations de milliards de symboles^[43]. Cependant, dans la plupart des cas, par exemple pour le groupe Bébé Monstre, ces calculs furent par la suite remplacés par des démonstrations plus courtes et plus conceptuelles^[44].
• 2004 : vérification de l'hypothèse de Riemann pour les premiers 10¹³ zéros de la fonction zêta^[45].
• 2008 : démonstration de la primalité de certains nombres de Mersenne ayant plus de dix millions de chiffres^[46].
• 2010 : démonstration de ce que le Rubik's Cube peut être résolu en 20 mouvements^[47].
• 2012 : le calcul de nombres de Ramsey (et même simplement de bornes assez étroites de ces nombres) demande la manipulation d'un nombre énorme de configurations^{[N 15]} ; ainsi, en 2012, Hiroshi Fujita a démontré que R(4,8) > 57 (la borne précédente était R(4,8)> 55), en 21 jours de calculs^[48].
• 2013 : le théorème de Feit-Thompson est démontré en Coq^[49],[50].
• À partir de 2005, l'apparition de solveurs SAT efficaces permet d'aborder certains problèmes analogues, au prix d'énormes volumes de sorties. Ainsi :
  • 2014 : la conjecture d'irrégularité d'Erdős (en) est démontrée dans le cas C=2 à l'aide d'un programme dont la sortie est constituée de 13 Go de données (treize milliards de caractères)^[51] ;
  • 2016 : le problème de bicoloration des triplets pythagoriciens est résolu par un calcul occupant 200 To (deux-cent mille milliards de caractères)^[52] ;
  • 2017 : le calcul du cinquième nombre de Schur, S(5) = 161, a une démonstration occupant 2 Po (deux millions de milliards de caractères)^[53] ;
  • 2022 : calcul de cent mille milliards (10¹⁴) de décimales de π par Emma Haruka Iwao^[54].

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « List of long proofs » (voir la liste des auteurs).

• Jean-Paul Delahaye, « Du rêve à la réalité des preuves », Pour la science, Paris, n^o 402,‎ 2011 (lire en ligne)
• Jean-Paul Delahaye, « Comment vérifier les longues démonstrations », Pour la science, Paris, n^o 452,‎ 2015 (résumé)
• (en) Steven G. Krantz, The proof is in the pudding. The changing nature of mathematical proof, Berlin, New York, Springer-Verlag, 2011 (lire en ligne)
• (en) Pavel Pudlák, Handbook of proof theory, Elsevier (éditeur Samuel Buss), 1998, « Chapitre 8 : The Lengths of Proofs », p. 548-642 (lire en ligne)

• Sur le blog de Jean-Paul Delahaye :
  • Incomplétude et complexité des démonstrations
  • La complexité mathématique est sans limite
  • Une très longue démonstration

• Portail des mathématiques
• Portail de la logique