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 , 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ésultatsVoir par exemple l'introduction du traité de Nicolas Bourbaki (Ens,I, p. 7-12). 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 courtesCette discussion (en anglais) sur le site de MathOverflow donne quelques exemples de ce que des mathématiciens professionnels contemporains jugent particulièrement élégant ; d'autres discussions du même genre (par exemple celle-ci) renvoient souvent au livre Raisonnements divins mentionné au paragraphe suivant..
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éIl suffirait en effet d'explorer toutes les démonstrations possibles de longueur inférieure à celle qui est connue ; en pratique, toutefois, une telle recherche est matériellement impossible sous cette forme, en raison de l'explosion combinatoire.) 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 », p. 26. 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 , 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 , 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 MathematicaVoir à ce sujet ces analyses (en anglais) sur le blog de ; Scott Aaronson fait en particulier remarquer que le problème n'est pas l'apparition de difficultés mathématiques subtiles qui demanderaient de longs préliminaires pour aboutir à une rigueur absolue, mais seulement la nécessité de spécifier correctement tous les détails du langage utilisé, parmi lesquels la définition de 1, 2 et +., 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 symbolesDelahaye précise qu'il en faudrait .... 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 exactitude.Des projets de vérification automatique tels que le projet Flyspeck sont d'ailleurs déjà utilisés pour assurer la correction de certaines des longues démonstrations citées plus loin..
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. 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 cohPA, 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.
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 ; une analyse plus précise de ce résultat, utilisant la fonction du castor affairé, a été donnée par Gustavo Lacerda en 2014.
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 lignes.. 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-exemple : ; 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é : .
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 Paolo Ruffini, Teoria generale delle equazioni in cui si dimostra impossibile la soluzione algebrica delle equazioni generali di grado superiore al quarto, nella stamperia di S. Tommaso d'Aquino(IS), S. Tommaso d'Aquino (tip.), 1799, 509 pages (lire en ligne)., 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 en 4 articles, I, II, III et IV.. 1894 : La construction du polygone régulier à par occupe plus de (Sur la division du cercle en 65537 parties égales).. 1905 : La démonstration initiale par Emanuel Lasker du théorème de décomposition primaire prenait ; on peut à présent le démontrer en moins d'une page ; on trouvera une démonstration moderne (et courte) dans l’Introduction to commutative algebra de Michael Atiyah et Ian G. Macdonald (lire en ligne, théorèmes 4.5 et 4.10).. 1963 : La démonstration du théorème de l'ordre impair par Feit et Thompson prend . Consultation payante en ligne. (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, est encore considéré comme long pour un article de théorie des groupes. 1964 : Heisuke Hironaka démontre en que toutes les singularités des variétés algébriques (de caractéristique nulle) sont (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 . (en 2009, Cutkosky la simplifie pour la ramener à .). 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 ; son prolongement par l'étude du théorème de Plancherel pour les groupes semi-simples occupe supplémentaires V. S. Varadarajan, « Harish-Chandra and his mathematical work », Current Sci., vol. 65, , 1993, .. 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 Voir l'historique au début de cet article de Mikhaïl Gromov et Thomas Delzant.. 1960 à 1970 : Alexandre Grothendieck publie Fondements de la géométrie algébrique (FGA, plus de ), Éléments de géométrie algébrique (EGA, ) 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 1974Voir cette présentation des travaux de Grothendieck par Jean Dieudonné en 1966 ; un dossier plus complet (vulgarisant l'ensemble de son œuvre) a été publié par La Recherche en avril 2014.. 1974 : Thompson achève la dans une série de 6 articles totalisant environ , et s'appuyant également sur le théorème de l'ordre impair, ce qui porterait la longueur totale à plus de ..