Longueur d'une démonstration

Un article de Wikipédia, l'encyclopédie libre.

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 XXe 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[modifier | modifier le code]

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 XXe 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[modifier | modifier le code]

Articles détaillés : Théorème d'accélération de Gödel et Théorème de Kruskal.

L'idée de l'utilisation d'un langage formel pour la rédaction de démonstrations mathématiques nait, à la fin du XIXe 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 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.

Démonstrations courtes[modifier | modifier le code]

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[5]. Notamment :

  • la conjecture d'Euler énoncée en 1772 n'a été réfutée qu'en 1966[6], la démonstration se résumant à l'énoncé d'un contre-exemple[N 6] : 275 + 845 + 1105 + 1335 = 1445 ;
  • la conjecture de Simpson énoncée en 1987[7] a de même été réfutée en 1989[8] par le simple énoncé : D = {6, 15, 35, 14, 210 (140 fois).

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

Démonstrations longues[modifier | modifier le code]

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.

Calculs et démonstrations assistés par ordinateur[modifier | modifier le code]

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[39]. 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 12].

Notes[modifier | modifier le code]

  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.
  4. ↑ 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 +.
  5. ↑ 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.
  6. ↑ Le contre-exemple tient en 22 caractères d'imprimerie, et l'article en 5 lignes (12 en incluant le titre, les auteurs et la référence)[6].
  7. ↑ 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.
  8. ↑ Corpus dont on peut se faire une idée en lisant l'article consacré à cette démonstration (en).
  9. ↑ Voir par exemple les Notes on Perelman Papers (en) de Bruce Kleiner et John Lott, publiées en 2013.
  10. ↑ 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.
  11. ↑ 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.
  12. ↑ 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 XIXe siècle, tâche ayant parfois pris de longues années ; voir par exemple les articles consacrés à William Shanks ou Fortuné Landry.
  13. ↑ 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, , p. 4).

Références[modifier | modifier le code]

  1. ↑ (en) Paul Hoffman, The Man Who Loved Only Numbers: The Story of Paul Erdős and the Search for Mathematical Truth, Fourth Estate Ltd, (lire en ligne), p. 26
  2. ↑ Paul Beame et Toniann Pitassi, « Propositional proof complexity: past, present, and future », Bulletin of the European Association for Theoretical Computer Science, no 65,‎ , p. 66-89.
  3. ↑ Delahaye (Delahaye 2011) précise qu'il en faudrait 4 523 659 424 929...
  4. ↑ Delahaye 2011
  5. ↑ a et b Jean-Paul Delahaye, « Florilège de records en science », Pour la science, no 544,‎ , p. 80-85.
  6. ↑ a et b (en) L. J. Lander et T. R. Parkin, « Counterexample to Euler's conjecture on sums of like powers », Bulletin of the American Mathematical Society, vol. 72, no 6,‎ , p. 1079 (DOI 10.1090/S0002-9904-1966-11654-3 Accès libre, lire en ligne Accès libre [PDF], consulté le ).
  7. ↑ (en) R. J. Simpson, « Disjoint Covering Systems of Congruences », The American Mathematical Monthly, vol. 94, no 9,‎ , p. 865-868 (DOI 10.1080/00029890.1987.12000731 Accès libre).
  8. ↑ (en) Doron Zeilberger, « On a Conjecture of R. J. Simpson About Exact Covering Congruences », The American Mathematical Monthly, vol. 96, no 3,‎ , p. 243 (DOI 10.1080/00029890.1989.11972176 Accès libre).
  9. ↑ (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).
  10. ↑ (en) John J. O'Connor et Edmund F. Robertson, « Niels Henrik Abel », sur MacTutor, université de St Andrews..
  11. ↑ (de) Wilhelm Killing, « Die Zusammensetzung der stetigen/endlichen Transformationsgruppen », Math. Ann.,‎ 1888-90, I, II, III et IV.
  12. ↑ (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,‎ , p. 186-418 (lire en ligne) (Sur la division du cercle en 65537 parties égales).
  13. ↑ (de) Emanuel Lasker, « Zur Theorie der Moduln und Ideale », Mathematische Annalen, vol. 60,‎ , 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).
  14. ↑ (en) Walter Feit et John G. Thompson, « Solvability of groups of odd order », Pac. J. Math., vol. 13,‎ , p. 775-1029. Consultation payante en ligne.
  15. ↑ G. Gonthier et al., « A Machine-Checked Proof of the Odd Order Theorem », HAL, Archives ouvertes,‎ (lire 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, no 3,‎ , p. 323-403 (lire en ligne).
  17. ↑ (en) Shreeram S. Abhyankar, Resolution of singularities of embedded algebraic surfaces, Berlin, Academic Press, , 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, , 59-127 p. (JSTOR 40068184, MR 2488485), chap. 1.
  19. ↑ (en) V. S. Varadarajan, « Harish-Chandra and his mathematical work », Current Sci., vol. 65, no 12, 1993, p. 918-919.
  20. ↑ Voir l'historique au début de cet article de Mikhaïl Gromov et Thomas Delzant.
  21. ↑ (en) Daniel Gorenstein, Finite Groups, New York, Chelsea, , 519 p. (ISBN 978-0-8284-0301-6, MR 81b:20002).
  22. ↑ Pierre Deligne, « La conjecture de Weil. I », Publ. Math. IHES, n° 43, 1974, p. 273-307.
  23. ↑ (en) Remise du prix Abel 2013.
  24. ↑ (en) Kenneth Appel et Wolfgang Haken, « Every Planar Map is Four Colorable Part I. Discharging », Illinois Journal of Mathematics, vol. 21,‎ , 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,‎ , p. 491-567.
  25. ↑ (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 », , 464 p. (ISBN 978-0-8218-1847-3, MR 0367048, lire en ligne).
  26. ↑ (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).
  27. ↑ (en) D. Gorenstein et Richard Lyons, « The local structure of finite groups of characteristic 2 type », Memoirs of the American Mathematical Society, vol. 42, no 276,‎ , vii+731 (ISBN 978-0-8218-2276-0, ISSN 0065-9266, MR 690900, lire en ligne).
  28. ↑ (en) Michael Aschbacher, « Finite groups of rank 3. I et II », Inventiones Mathematicae, vol. 63, pages 357-402 et 71, pages 51-163, no 3,‎ (DOI 10.1007/BF01389061, MR 620676).
  29. ↑ (en) Dennis Hejhal, The Selberg Trace Formula for PSL (2, R), 2 volumes, Springer, 1976 (un troisième volume est prévu).
  30. ↑ (en) Patterson, S. J., « Review: Dennis A. Hejhal, The Selberg trace formula for PSL(2, R), Volume I », Bull. Amer. Math. Soc., vol. 84, no 2,‎ , p. 256-260 (DOI 10.1090/s0002-9904-1978-14466-8, lire en ligne).
  31. ↑ (en) Stephen Gelbart, Lectures on the Arthur-Selberg trace formula, vol. 9, Providence, R.I., AMS, coll. « University Lecture Series », (lire en ligne).
  32. ↑ (en) Andrew Wiles, « Modular elliptic curves and Fermat's last theorem », Ann. Math., vol. 141,‎ , p. 443-551 (lire en ligne).
  33. ↑ (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 », , 955 p. (ISBN 978-981-02-4108-7, lire en ligne).
  34. ↑ Michael Rapoport, The work of Laurent Lafforgue (lire en ligne (en)).
  35. ↑ (en) (avec Stephen D. Smith), The Classification of Quasithin Groups : I Structure of Strongly Quasithin K-groups, AMS, coll. « Mathematical Surveys and Monographs » (no 111), , 1221 p. (ISBN 978-0-8218-3410-7, présentation en ligne, lire en ligne).
  36. ↑ (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 » (no 112), , 1221 p. (ISBN 978-0-8218-3411-4, présentation en ligne).
  37. ↑ Une analyse détaillée de la situation au début des années 2000 figure dans Krantz 2011, p. 186 à 191.
  38. ↑ (en) Maria Chudnovsky, Neil Robertson, Paul Seymour et Robin Thomas, « The strong perfect graph theorem », Ann. Math., vol. 164, no 1,‎ , p. 51-229 (lire en ligne).
  39. ↑ Michèle Artigue, Calcul et démonstration (lire en ligne)
  40. ↑ (en) Charles C. Sims, Finite groups '72 (Proc. Gainesville Conf., Univ. Florida, Gainesville, Fla., 1972), vol. 7, Amsterdam, North-Holland, , 138–141 p., « The existence and uniqueness of Lyons' group »
  41. ↑ (en) Daniel Gorenstein, The Gelʹfand Mathematical Seminars, 1990–1992, Boston, MA, Birkhäuser Boston, , 137–143 p. (ISBN 978-0-8176-3689-0, MR 1247286, lire en ligne), « A brief history of the sporadic simple groups »
  42. ↑ (en) X. Gourdon, « The 1013 first zeros of the Riemann zeta function, and zeros computation at very large height », une version consultable en ligne,‎ , voir aussi (en) Computation of zeros of the zeta function
  43. ↑ 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.
  44. ↑ (en) Détails du calcul sur le site de l'équipe l'ayant effectué
  45. ↑ (en) Hiroshi Fujita, A New Lower Bound for the Ramsey Number R(4,8) (lire en ligne)
  46. ↑ Feit-Thompson theorem has been totally checked in Coq
  47. ↑ 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
  48. ↑ (en) Boris Konev et Alexei Lisitsa, « A SAT Attack on the Erdos Discrepancy Conjecture », ArXiv,‎ (arXiv 1402.2184) ; voir aussi ce commentaire de Jacob Aron (en) dans New Scientist.
  49. ↑ La plus grosse preuve de l'histoire des mathématiques, Journal du CNRS.
  50. ↑ (en) Heule, Marijn JH., « Schur Number Five », arXiv:1711.08076,‎ (lire en ligne).
  51. ↑ (en) Calcul de cent trillions de décimales de pi sur Google Cloud

Bibliographie[modifier | modifier le code]

Liens externes[modifier | modifier le code]

Ce document provient de « https://fr.wikipedia.org/w/index.php?title=Longueur_d%27une_démonstration&oldid=208493741 ».