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

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[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 simples finis, 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 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. 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.

Liste de longues démonstrations ayant été publiées

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 simples finis, 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[5], fut pour l'essentiel ignorée ; en 1824, Niels Henrik Abel publia une démonstration ne comportant que six pages[6].
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[7].
1894 : La construction du polygone régulier à 65 537 côtés par Johann Gustav Hermes (en) occupe plus de 200 pages[8].
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[9].
1963 : La démonstration du théorème de l'ordre impair par Feit et Thompson prend 255 pages[10] (mais a été substantiellement simplifiée depuis par Gonthier et son équipe pour pouvoir mener à bien leur démonstration certifiée par ordinateur^{[réf. souhaitée]}) ; à 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)[11].
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[12] (en 2009, Cutkosky la simplifie pour la ramener à 40 pages[13]).
1966 : La construction par Harish-Chandra des représentations par séries discrètes (en) 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[14].
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[15].
1960 à 1970 : Alexandre Grothendieck publie Fondements de la géométrie algébrique (FGA, plus de 1000 pages), Éléments de géométrie algébrique (EGA, 1500 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 6].
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[16].
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[17], 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 2000 pages[18].
1974 : La démonstration d'Appel et Haken du théorème des quatre couleurs prend 139 pages[19], 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 simples finis) occupe 464 pages[20].
1976 : La construction par Robert Langlands de l'équation fonctionnelle des séries d'Eisenstein occupe 337 pages[21].
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[22] ; la démonstration par Aschbacher du cas du rang 3 occupe 159 pages supplémentaires[23].
1983 : La démonstration par Dennis Hejhal (en) d'une généralisation de la formule des traces de Selberg occupe 2 volumes d'un total de 1322 pages[24]^,[25].
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[26].
1995 : La démonstration par Andrew Wiles du dernier théorème de Fermat ne comporte « que » 108 pages[27], mais s'appuie sur un énorme corpus de résultats préliminaires[N 7].
2000 : La démonstration par Almgren de son théorème de régularité (en) occupe 955 pages[28].
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[29].
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 8].
2004 : La classification des groupes quasi-fins (en) par Michael Aschbacher et Stephen Smith prend 1221 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[30]^,[31]. Ces deux articles veulent mettre un point final à la classification des groupes finis simples.
2004 : Classification des groupes simples finis. 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[32]. 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 9].
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[33].
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 10].

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[34]. 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, 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 2014) 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 11] :

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[35]. 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[36].
2004 : Vérification de l'hypothèse de Riemann pour les premiers 10¹³ zéros de la fonction zêta[37].
2008 : Démonstration de la primalité de certains nombres de Mersenne ayant plus de dix millions de chiffres[38].
2010 : Démonstration de ce que le Rubik's Cube peut être résolu en 20 mouvements[39].
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 12] ; 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[40].
2013 : Calcul de plus de douze mille milliards (1.21 10¹³) de décimales de π[41].
2013 : Le théorème de Feit-Thompson est démontré en Coq[42]^,[43].
À 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 gigaoctets de données[44].
- 2016 : Le problème de bicoloration (en) des triplets pythagoriciens est résolu par un calcul occupant 200 téraoctets[45].
- 2017 : Le calcul du cinquième nombre de Schur, S(5) = 161, a une démonstration occupant 2 pétaoctets[46].

Notes

Voir par exemple l'introduction du traité de Nicolas Bourbaki (Ens,I, p. 7-12)
Cette 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.
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.
Voir à ce sujet ces analyses (en anglais) sur le blog de Lance Fortnow (en) ; 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 +.
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.
Voir 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.
Corpus dont on peut se faire une idée en lisant l'article consacré à cette démonstration (en).
Voir par exemple les Notes on Perelman Papers (en) de Bruce Kleiner et John Lott, publiées en 2013.
L'analyse de l'enchaînement des résultats aboutissant à cette démonstration figure dans (en) Reinhard Diestel, Graph Theory [détail des éditions], p. 373.
La démonstration initiale de Hales (en 1998) n'a pas été vraiment acceptée, ce qui l'a amené à la réécrire sous une forme en permettant une vérification automatique (c'est le projet Flyspeck) ; bien que ce dernier ne se soit achevé qu'en août 2014, Hales avait déjà reçu le prix Fulkerson en 2009, ce qu'on peut interpréter comme une reconnaissance officielle de la validité de sa démonstration.
Ainsi, 2047 décimales de Pi furent calculées en 1949 par ENIAC, un des premiers ordinateurs. Mais en fait, certains de ces calculs avaient même été effectués à la main dès le XIX^e siècle, tâche ayant parfois pris de longues années ; voir par exemple les articles consacrés à William Shanks ou Fortuné Landry.
Paul Erdős estimait que « en combinant toutes nos ressources, nous pourrions envisager de calculer R(5,5) si des extraterrestres nous menaçaient de destruction en cas d'échec, mais s'ils nous demandaient de calculer R(6,6), nous ferions mieux de tenter de leur résister » ((en) Joel H. Spencer, Ten Lectures on the Probabilistic Method, SIAM, 1994, p. 4).

Références

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

(en) Paul Hoffman, The Man Who Loved Only Numbers (en): The Story of Paul Erdős and the Search for Mathematical Truth, Fourth Estate Ltd, 1998 (lire en ligne), p. 26
Paul Beame et Toniann Pitassi, « Propositional proof complexity: past, present, and future », Bulletin of the European Association for Theoretical Computer Science, n^o 65,‎ 1998, p. 66-89.
Delahaye (Delahaye 2011) précise qu'il en faudrait 4 523 659 424 929...
Delahaye 2011
(it) 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).
(en) John J. O'Connor et Edmund F. Robertson, « Niels Henrik Abel », dans MacTutor History of Mathematics archive, université de St Andrews (lire en ligne)..
(de) Wilhelm Killing, « Die Zusammensetzung der stetigen/endlichen Transformationsgruppen », Math. Ann.,‎ 1888-90, I, II, III et IV.
(de) Johann Gustav Hermes, « Über die Teilung des Kreises in 65537 gleiche Teile », Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, Göttingen, vol. 3,‎ 1894, p. 186-418 (lire en ligne) (Sur la division du cercle en 65537 parties égales).
(de) Emanuel Lasker, « Zur Theorie der Moduln und Ideale », Mathematische Annalen, vol. 60,‎ 1905, p. 20-116 ; 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).
(en) Walter Feit et John G. Thompson, « Solvability of groups of odd order », Pac. J. Math., vol. 13,‎ 1963, p. 775-1029. Consultation payante en ligne.
(en) Herwig Hauser, « The Hironaka theorem on resolution of singularities (or: A proof we always wanted to understand) », Bull. Amer. Math. Soc. (N.S.), vol. 40, n^o 3,‎ 2003, p. 323-403 (lire en ligne).
(en) Shreeram S. Abhyankar, Resolution of singularities of embedded algebraic surfaces, Berlin, Academic Press, 1966, 311 p. (ISBN 3-540-63719-2, lire en ligne).
(en) Steven Dale Cutkosky, Resolution of singularities for 3-folds in positive characteristic, vol. 131, 2009, 59-127 p. (JSTOR 40068184, Math Reviews 2488485), chap. 1.
(en) V. S. Varadarajan, « Harish-Chandra and his mathematical work », Current Sci., vol. 65, n^o 12, 1993, p. 918-919.
Voir l'historique au début de cet article de Mikhaïl Gromov et Thomas Delzant.
(en) Daniel Gorenstein, Finite Groups, New York, Chelsea, 1980, 519 p. (ISBN 978-0-8284-0301-6, Math Reviews 81b:20002).
Pierre Deligne, « La conjecture de Weil. I », Publ. Math. IHES, n° 43, 1974, p. 273-307.
(en) Remise du prix Abel 2013.
(en) Kenneth Appel et Wolfgang Haken, « Every Planar Map is Four Colorable Part I. Discharging », Illinois Journal of Mathematics, vol. 21,‎ 1977, p. 429-490 ; (en) Kenneth Appel, Wolfgang Haken et John Koch, « Every Planar Map is Four Colorable Part II. Reducibility », Illinois Journal of Mathematics, vol. 21,‎ 1977, p. 491-567.
(en) D. Gorenstein et Koichiro Harada, Finite groups whose 2-subgroups are generated by at most 4 elements, vol. 147, Providence, R.I., AMS, coll. « Memoirs of the American Mathematical Society », 1974, 464 p. (ISBN 978-0-8218-1847-3, Math Reviews 0367048, lire en ligne).
(en) R. P. Langlands, On the Functional Equations Satisfied by Eisenstein Series, Lecture Notes in Math., vol. 544, Springer-Verlag, Berlin-Heidelberg-New York, 1976. (lire en ligne).
(en) D. Gorenstein et Richard Lyons, « The local structure of finite groups of characteristic 2 type », Memoirs of the American Mathematical Society, vol. 42, n^o 276,‎ 1983, vii+731 (ISBN 978-0-8218-2276-0, ISSN 0065-9266, Math Reviews 690900, lire en ligne).
(en) Michael Aschbacher, « Finite groups of rank 3. I et II », Inventiones Mathematicae, vol. 63, pages 357-402 et 71, pages 51-163, n^o 3,‎ 1981 (DOI 10.1007/BF01389061, Math Reviews 620676).
(en) Dennis Hejhal, The Selberg Trace Formula for PSL (2, R), 2 volumes, Springer, 1976 (un troisième volume est prévu).
(en) Patterson, S. J., « Review: Dennis A. Hejhal, The Selberg trace formula for PSL(2, R), Volume I », Bull. Amer. Math. Soc., vol. 84, n^o 2,‎ 1978, p. 256-260 (DOI 10.1090/s0002-9904-1978-14466-8, lire en ligne).
(en) Stephen Gelbart, Lectures on the Arthur-Selberg trace formula, vol. 9, Providence, R.I., AMS, coll. « University Lecture Series », 1996 (lire en ligne).
(en) Andrew Wiles, « Modular elliptic curves and Fermat's last theorem », Ann. Math., vol. 141,‎ 1995, p. 443-551 (lire en ligne).
(en) Frederick J. Jr. Almgren, Jean E. Taylor (dir.) et Vladimir Scheffer (dir.), Almgren's Big Regularity Paper, vol. 1, World Scientific, coll. « World Scientific Monograph Series in Mathematics », 2000, 955 p. (ISBN 978-981-02-4108-7, lire en ligne).
Michael Rapoport, The work of Laurent Lafforgue (lire en ligne (en)).
(en) (avec Stephen D. Smith), The Classification of Quasithin Groups : I Structure of Strongly Quasithin K-groups, AMS, coll. « Mathematical Surveys and Monographs » (n^o 111), 2004, 1221 p. (ISBN 978-0-8218-3410-7, présentation en ligne, lire en ligne).
(en) (avec Stephen D. Smith), The Classification of Quasithin Groups : II Main Theorems: The Classification of Simple QTKE-groups, AMS, coll. « Mathematical Surveys and Monographs » (n^o 112), 2004, 1221 p. (ISBN 978-0-8218-3411-4, présentation en ligne).
Une analyse détaillée de la situation au début des années 2000 figure dans Krantz 2011, p. 186 à 191.
(en) Maria Chudnovsky, Neil Robertson, Paul Seymour et Robin Thomas, « The strong perfect graph theorem », Ann. Math., vol. 164, n^o 1,‎ 2006, p. 51-229 (lire en ligne).
Michèle Artigue, Calcul et démonstration (lire en ligne)
(en) Charles C. Sims, Finite groups '72 (Proc. Gainesville Conf., Univ. Florida, Gainesville, Fla., 1972), vol. 7, Amsterdam, North-Holland, 1973, 138–141 p., « The existence and uniqueness of Lyons' group »
(en) Daniel Gorenstein, The Gelʹfand Mathematical Seminars, 1990–1992, Boston, MA, Birkhäuser Boston, 1993, 137–143 p. (ISBN 978-0-8176-3689-0, Math Reviews 1247286, lire en ligne), « A brief history of the sporadic simple groups »
(en) X. Gourdon, « The 10¹³ first zeros of the Riemann zeta function, and zeros computation at very large height », une version consultable en ligne,‎ octobre 2004, voir aussi (en) Computation of zeros of the zeta function
Voir la page d'accueil (en) du projet GIMPS ; en 2014, le record est détenu par un nombre ayant plus de 17 millions de chiffres.
(en) Détails du calcul sur le site de l'équipe l'ayant effectué
(en) Hiroshi Fujita, A New Lower Bound for the Ramsey Number R(4,8) (lire en ligne)
(en) Détails du calcul par Alexander J. Yee et Shigeru Kondo
Feit-Thompson theorem has been totally checked in Coq
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry: A Machine-Checked Proof of the Odd Order Theorem. ITP 2013: 163-179
(en) Boris Konev et Alexei Lisitsa, « A SAT Attack on the Erdos Discrepancy Conjecture », ArXiv,‎ 17 février 2014 (arXiv 1402.2184) ; voir aussi ce commentaire de Jacob Aron (en) dans New Scientist.
La plus grosse preuve de l'histoire des mathématiques, Journal du CNRS.
(en) Heule, Marijn JH., « Schur Number Five », arXiv:1711.08076,‎ 2017 (lire en ligne).

Bibliographie

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)

Liens externes

Sur le blog de Jean-Paul Delahaye :

Portail des mathématiques
Portail de la logique

Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.

[1] Voir par exemple l'introduction du traité de Nicolas Bourbaki (Ens,I, p. 7-12)

[2] Cette 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.

[3] 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.

[6] Voir à ce sujet ces analyses (en anglais) sur le blog de Lance Fortnow (en) ; 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 +.

[9] 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.

[21] Voir 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.

[34] Corpus dont on peut se faire une idée en lisant l'article consacré à cette démonstration (en).

[37] Voir par exemple les Notes on Perelman Papers (en) de Bruce Kleiner et John Lott, publiées en 2013.

[41] L'analyse de l'enchaînement des résultats aboutissant à cette démonstration figure dans (en) Reinhard Diestel, Graph Theory [détail des éditions], p. 373.

[43] La démonstration initiale de Hales (en 1998) n'a pas été vraiment acceptée, ce qui l'a amené à la réécrire sous une forme en permettant une vérification automatique (c'est le projet Flyspeck) ; bien que ce dernier ne se soit achevé qu'en août 2014, Hales avait déjà reçu le prix Fulkerson en 2009, ce qu'on peut interpréter comme une reconnaissance officielle de la validité de sa démonstration.

[45] Ainsi, 2047 décimales de Pi furent calculées en 1949 par ENIAC, un des premiers ordinateurs. Mais en fait, certains de ces calculs avaient même été effectués à la main dès le XIX^e siècle, tâche ayant parfois pris de longues années ; voir par exemple les articles consacrés à William Shanks ou Fortuné Landry.

[51] Paul Erdős estimait que « en combinant toutes nos ressources, nous pourrions envisager de calculer R(5,5) si des extraterrestres nous menaçaient de destruction en cas d'échec, mais s'ils nous demandaient de calculer R(6,6), nous ferions mieux de tenter de leur résister » ((en) Joel H. Spencer, Ten Lectures on the Probabilistic Method, SIAM, 1994, p. 4).

[4] (en) Paul Hoffman, The Man Who Loved Only Numbers (en): The Story of Paul Erdős and the Search for Mathematical Truth, Fourth Estate Ltd, 1998 (lire en ligne), p. 26

[BeameP98-5] Paul Beame et Toniann Pitassi, « Propositional proof complexity: past, present, and future », Bulletin of the European Association for Theoretical Computer Science, n^o 65,‎ 1998, p. 66-89.

[7] Delahaye (Delahaye 2011) précise qu'il en faudrait 4 523 659 424 929...

[Delahaye-8] Delahaye 2011

[10] (it) 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).

[11] (en) John J. O'Connor et Edmund F. Robertson, « Niels Henrik Abel », dans MacTutor History of Mathematics archive, université de St Andrews (lire en ligne)..

[12] (de) Wilhelm Killing, « Die Zusammensetzung der stetigen/endlichen Transformationsgruppen », Math. Ann.,‎ 1888-90, I, II, III et IV.

[13] (de) Johann Gustav Hermes, « Über die Teilung des Kreises in 65537 gleiche Teile », Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, Göttingen, vol. 3,‎ 1894, p. 186-418 (lire en ligne) (Sur la division du cercle en 65537 parties égales).

[14] (de) Emanuel Lasker, « Zur Theorie der Moduln und Ideale », Mathematische Annalen, vol. 60,‎ 1905, p. 20-116 ; 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).

[15] (en) Walter Feit et John G. Thompson, « Solvability of groups of odd order », Pac. J. Math., vol. 13,‎ 1963, p. 775-1029. Consultation payante en ligne.

[16] (en) Herwig Hauser, « The Hironaka theorem on resolution of singularities (or: A proof we always wanted to understand) », Bull. Amer. Math. Soc. (N.S.), vol. 40, n^o 3,‎ 2003, p. 323-403 (lire en ligne).

[17] (en) Shreeram S. Abhyankar, Resolution of singularities of embedded algebraic surfaces, Berlin, Academic Press, 1966, 311 p. (ISBN 3-540-63719-2, lire en ligne).

[18] (en) Steven Dale Cutkosky, Resolution of singularities for 3-folds in positive characteristic, vol. 131, 2009, 59-127 p. (JSTOR 40068184, Math Reviews 2488485), chap. 1.

[19] (en) V. S. Varadarajan, « Harish-Chandra and his mathematical work », Current Sci., vol. 65, n^o 12, 1993, p. 918-919.

[20] Voir l'historique au début de cet article de Mikhaïl Gromov et Thomas Delzant.

[22] (en) Daniel Gorenstein, Finite Groups, New York, Chelsea, 1980, 519 p. (ISBN 978-0-8284-0301-6, Math Reviews 81b:20002).

[23] Pierre Deligne, « La conjecture de Weil. I », Publ. Math. IHES, n° 43, 1974, p. 273-307.

[24] (en) Remise du prix Abel 2013.

[25] (en) Kenneth Appel et Wolfgang Haken, « Every Planar Map is Four Colorable Part I. Discharging », Illinois Journal of Mathematics, vol. 21,‎ 1977, p. 429-490 ; (en) Kenneth Appel, Wolfgang Haken et John Koch, « Every Planar Map is Four Colorable Part II. Reducibility », Illinois Journal of Mathematics, vol. 21,‎ 1977, p. 491-567.

[26] (en) D. Gorenstein et Koichiro Harada, Finite groups whose 2-subgroups are generated by at most 4 elements, vol. 147, Providence, R.I., AMS, coll. « Memoirs of the American Mathematical Society », 1974, 464 p. (ISBN 978-0-8218-1847-3, Math Reviews 0367048, lire en ligne).

[27] (en) R. P. Langlands, On the Functional Equations Satisfied by Eisenstein Series, Lecture Notes in Math., vol. 544, Springer-Verlag, Berlin-Heidelberg-New York, 1976. (lire en ligne).

[28] (en) D. Gorenstein et Richard Lyons, « The local structure of finite groups of characteristic 2 type », Memoirs of the American Mathematical Society, vol. 42, n^o 276,‎ 1983, vii+731 (ISBN 978-0-8218-2276-0, ISSN 0065-9266, Math Reviews 690900, lire en ligne).

[29] (en) Michael Aschbacher, « Finite groups of rank 3. I et II », Inventiones Mathematicae, vol. 63, pages 357-402 et 71, pages 51-163, n^o 3,‎ 1981 (DOI 10.1007/BF01389061, Math Reviews 620676).

[30] (en) Dennis Hejhal, The Selberg Trace Formula for PSL (2, R), 2 volumes, Springer, 1976 (un troisième volume est prévu).

[31] (en) Patterson, S. J., « Review: Dennis A. Hejhal, The Selberg trace formula for PSL(2, R), Volume I », Bull. Amer. Math. Soc., vol. 84, n^o 2,‎ 1978, p. 256-260 (DOI 10.1090/s0002-9904-1978-14466-8, lire en ligne).

[32] (en) Stephen Gelbart, Lectures on the Arthur-Selberg trace formula, vol. 9, Providence, R.I., AMS, coll. « University Lecture Series », 1996 (lire en ligne).

[33] (en) Andrew Wiles, « Modular elliptic curves and Fermat's last theorem », Ann. Math., vol. 141,‎ 1995, p. 443-551 (lire en ligne).

[35] (en) Frederick J. Jr. Almgren, Jean E. Taylor (dir.) et Vladimir Scheffer (dir.), Almgren's Big Regularity Paper, vol. 1, World Scientific, coll. « World Scientific Monograph Series in Mathematics », 2000, 955 p. (ISBN 978-981-02-4108-7, lire en ligne).

[36] Michael Rapoport, The work of Laurent Lafforgue (lire en ligne (en)).

[38] (en) (avec Stephen D. Smith), The Classification of Quasithin Groups : I Structure of Strongly Quasithin K-groups, AMS, coll. « Mathematical Surveys and Monographs » (n^o 111), 2004, 1221 p. (ISBN 978-0-8218-3410-7, présentation en ligne, lire en ligne).

[39] (en) (avec Stephen D. Smith), The Classification of Quasithin Groups : II Main Theorems: The Classification of Simple QTKE-groups, AMS, coll. « Mathematical Surveys and Monographs » (n^o 112), 2004, 1221 p. (ISBN 978-0-8218-3411-4, présentation en ligne).

[40] Une analyse détaillée de la situation au début des années 2000 figure dans Krantz 2011, p. 186 à 191.

[42] (en) Maria Chudnovsky, Neil Robertson, Paul Seymour et Robin Thomas, « The strong perfect graph theorem », Ann. Math., vol. 164, n^o 1,‎ 2006, p. 51-229 (lire en ligne).

[44] Michèle Artigue, Calcul et démonstration (lire en ligne)

[46] (en) Charles C. Sims, Finite groups '72 (Proc. Gainesville Conf., Univ. Florida, Gainesville, Fla., 1972), vol. 7, Amsterdam, North-Holland, 1973, 138–141 p., « The existence and uniqueness of Lyons' group »

[47] (en) Daniel Gorenstein, The Gelʹfand Mathematical Seminars, 1990–1992, Boston, MA, Birkhäuser Boston, 1993, 137–143 p. (ISBN 978-0-8176-3689-0, Math Reviews 1247286, lire en ligne), « A brief history of the sporadic simple groups »

[48] (en) X. Gourdon, « The 10¹³ first zeros of the Riemann zeta function, and zeros computation at very large height », une version consultable en ligne,‎ octobre 2004, voir aussi (en) Computation of zeros of the zeta function

[49] Voir la page d'accueil (en) du projet GIMPS ; en 2014, le record est détenu par un nombre ayant plus de 17 millions de chiffres.

[50] (en) Détails du calcul sur le site de l'équipe l'ayant effectué

[52] (en) Hiroshi Fujita, A New Lower Bound for the Ramsey Number R(4,8) (lire en ligne)

[53] (en) Détails du calcul par Alexander J. Yee et Shigeru Kondo

[54] Feit-Thompson theorem has been totally checked in Coq

[55] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry: A Machine-Checked Proof of the Odd Order Theorem. ITP 2013: 163-179

[56] (en) Boris Konev et Alexei Lisitsa, « A SAT Attack on the Erdos Discrepancy Conjecture », ArXiv,‎ 17 février 2014 (arXiv 1402.2184) ; voir aussi ce commentaire de Jacob Aron (en) dans New Scientist.

[57] La plus grosse preuve de l'histoire des mathématiques, Journal du CNRS.

[58] (en) Heule, Marijn JH., « Schur Number Five », arXiv:1711.08076,‎ 2017 (lire en ligne).