Longueur d'une démonstration

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 Modèle:S-, certaines résultats importants ont néanmoins fait l'objet de démonstrations, parfois assistées par ordinateur, d'une longueur exceptionnelle.

Longueur des démonstrations

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. 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.

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é) 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 ». Le domaine de la complexité des preuves établit des résultats sur les tailles minimales des démonstrations selon divers systèmes de preuves.

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 Modèle:S-, 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 2025, 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.

Analyse de la longueur des démonstrations en logique mathématique

L'idée de l'utilisation d'un langage formel pour la rédaction de démonstrations mathématiques nait, à la fin du Modèle:S, 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, 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. 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 Rocq de contrôler rigoureusement leur exactitudeModèle:,.

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 longueModèle:Note. 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-SeymourModèle:Note.

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 simpleModèle:Note ; une analyse plus précise de ce résultat, utilisant la fonction du castor affairé, a été donnée par Gustavo Lacerda en 2014Modèle:Note.

Démonstrations courtes

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 lignesModèle:,Modèle:Note. Notamment :

• la conjecture d'Euler, énoncée en 1772, n'a été réfutée qu'en 1966, la démonstration se résumant à l'énoncé d'un contre-exempleModèle:Note : Modèle:Nobr ;

• la conjecture de Simpson concernant les systèmes couvrants, énoncée en 1987, a de même été réfutée en 1989 par le simple énoncé : Modèle:Nobr.

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.

Démonstrations longues

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 Modèle:Nobr, fut pour l'essentiel ignorée ; en 1824, Niels Henrik Abel publia une démonstration ne comportant que six pages.
• 1890 : La classification par Wilhelm Killing des algèbres de Lie simples (y compris sa découverte des algèbres exceptionnelles), occupe Modèle:Nobr en 4 articles.
• 1894 : La construction du [[Théorème de Gauss-Wantzel|polygone régulier à Modèle:Unité]] par Modèle:Lien occupe plus de Modèle:Nobr.
• 1905 : La démonstration initiale par Emanuel Lasker du théorème de décomposition primaire prenait Modèle:Nobr ; on peut à présent le démontrer en moins d'une page.
• 1963 : La démonstration du théorème de l'ordre impair par Feit et Thompson prend Modèle:Nobr (mais a été substantiellement simplifiée depuis par Gonthier et son équipe pour pouvoir mener à bien leur démonstration certifiée par ordinateur) ; à cette époque, Modèle:Nobr est encore considéré comme long pour un article de théorie des groupesModèle:Référence souhaitée.
• 1964 : Heisuke Hironaka démontre en Modèle:Nobr que toutes les singularités des variétés algébriques (de caractéristique nulle) sont Modèle:Lien (cette démonstration a été simplifiée depuis jusqu'à une vingtaine de pages).
• 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 Modèle:Nobr (en 2009, Cutkosky la simplifie pour la ramener à Modèle:Nobr).
• 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 Modèle:Nobr ; son prolongement par l'étude du théorème de Plancherel pour les groupes semi-simples occupe Modèle:Nobr supplémentaires.
• 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 Modèle:Nobr.
• 1960 à 1970 : Alexandre Grothendieck publie Fondements de la géométrie algébrique (FGA, plus de Modèle:Nombre), Éléments de géométrie algébrique (EGA, Modèle:Nombre) 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.
• 1974 : Thompson achève la Modèle:Lien dans une série de 6 articles totalisant environ Modèle:Nobr, et s'appuyant également sur le théorème de l'ordre impair, ce qui porterait la longueur totale à plus de Modèle:Nobr.
• 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 » Modèle:Nobr, 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 Modèle:Nombre.
• 1974 : La démonstration d'Appel et Haken du théorème des quatre couleurs prend Modèle:Nobr, mais c'est sans compter de longs calculs sur ordinateur (voir à ce sujet la section suivante).
• 1974 : Le Modèle:Lien (un autre résultat partiel dont dépend le théorème de classification des groupes finis simples) occupe Modèle:Nobr.
• 1976 : La construction par Robert Langlands de l'équation fonctionnelle des séries d'Eisenstein occupe Modèle:Nobr.
• 1983 : Gorenstein et Lyons démontrent le Modèle:Lien dans le cas d'un rang > 3 dans un article de Modèle:Nobr ; la démonstration par Aschbacher du cas du rang 3 occupe Modèle:Nobr supplémentaires.
• 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 Modèle:NombreModèle:,.
• 1974-2003 : Les démonstrations par James Arthur de Modèle:Lien occupent plusieurs centaines de pages dans de nombreux articles.
• 1995 : La démonstration par Andrew Wiles du dernier théorème de Fermat ne comporte « que » Modèle:Nobr, mais s'appuie sur un énorme corpus de résultats préliminaires.
• 2000 : La démonstration par Almgren de Modèle:Lien occupe Modèle:Nobr.
• 2000 : La démonstration par Laurent Lafforgue de la Modèle:Lien sur les corps de fonctions prend environ Modèle:Nobr, sans compter un volume bien plus important de résultats préliminaires.
• 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.
• 2004 : La classification des Modèle:Lien par Michael Aschbacher et Stephen Smith prend Modèle:Nombre ; 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 sujetModèle:,. 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. 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 Modèle:Nobr, occupant 20 articles publiés au long de deux décennies.
• 2006 : La démonstration du théorème des graphes parfaits, par Maria Chudnovsky, Neil Robertson, Paul Seymour, et Robin Thomas, prend Modèle:Nobr des Annals of Mathematics.
• 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.

Calculs et démonstrations assistés par ordinateur

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. 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.

• 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. 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.
• 2004 : vérification de l'hypothèse de Riemann pour les premiers 10¹³ zéros de la fonction zêta.
• 2008 : démonstration de la primalité de certains nombres de Mersenne ayant plus de dix millions de chiffres.
• 2010 : démonstration de ce que le Rubik's Cube peut être résolu en 20 mouvements.
• 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 ; 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.
• 2013 : le théorème de Feit-Thompson est démontré en CoqModèle:,.
• À 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 Modèle:Lien est démontrée dans le cas C=2 à l'aide d'un programme dont la sortie est constituée de Modèle:Unité de données (treize milliards de caractères) ;
  • 2016 : le problème de bicoloration des triplets pythagoriciens est résolu par un calcul occupant Modèle:Unité (deux-cent mille milliards de caractères) ;
  • 2017 : le calcul du cinquième nombre de Schur, S(5) = 161, a une démonstration occupant Modèle:Unité (deux millions de milliards de caractères) ;
  • 2022 : calcul de cent mille milliards (10Modèle:14) de décimales de π par Emma Haruka Iwao.

Bibliographie

• Modèle:Article
• Modèle:Article
• Modèle:Ouvrage
• Modèle:Ouvrage (lire en ligne)

Liens externes

• 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