Discussion:Longueur d'une démonstration
Lemoine
modifierA propos de longueur de démonstrations, je signale le traité de Lemoine, Géométrographie ou art des constructions géométriques, paru en 1902, qui essaie de minimiser le nombre d'étapes dans la construction de figures de géométrie.Cordialement dit. Le tigre à dents de sabre.Claudeh5 (discuter) 13 juin 2014 à 19:44 (CEST)
- Oui, j'ai moins tenté de référencer les aspects concrets de la réduction de la longueur des preuves en langage naturel (faute de sources secondaires). --Dfeldmann (discuter) 14 juin 2014 à 03:00 (CEST)
Suggestions bibliographiques pour développer l'article, voire plus si on trouve des sources
modifierBonjour, en attendant peut-être de les exploiter moi-même, je signale l'existence de 2 articles, sur le blog de Delahaye sur le sujet :
- 1. une très longue démonstration
- 2. et surtout à un niveau plus théorique La complexité mathématique est sans limites dont la bibliographie, pas encore regardée, semble très motivante.
Il me semble en tout cas que la section Analyse de la longueur des démonstrations en logique mathématique, qui pourrait aussi faire l'objet d'un article dédié, mériterait des développements. ... incluant d'ailleurs aussi, mais là je n'ai pas de sources sous les doigts ː
- 3. Longueur des démonstrations selon que l'on utilise la règle de coupure ... ou pas
- 4. D'autres considérations comme ː le constat que sur un alphabet fini (cas p.-e. raisonnable ou au moins usuel) il n'y a qu'une infinité dénombrable de démonstrations (qui sont des suites finies de formules finies) donc forcément dès qu'on parle des réels on va tomber sur l'inexistence de démonstrations (notion distincte de l'incomplétude, hein ǃ).
Cordialement, --Epsilon0 ε0 20 février 2017 à 06:35 (CET)
Feit-Thompson
modifierL'article dit « La démonstration du théorème de l'ordre impair par Feit et Thompson prend 255 pages (et n'a pas été substantiellement simplifiée depuis) ». Je pense que ça n'a pas vrai. Car la mécanisation en Coq a nécessité des simplifications et les a mises en œuvre [1]. Je me souviens d'avoir entendu Gonthier évoquer sa lecture d'un livre décrivant la démonstration, où il avait vu du « code mort » (des parties ne servant à rien) et des duplications de démonstration. --Pierre de Lyon (discuter) 20 mars 2018 à 12:03 (CET)
Proposition d'anecdote pour la page d'accueil
modifierUne anecdote fondée sur cet article a été proposée ici (une fois acceptée ou refusée, elle est archivée là). N'hésitez pas à apporter votre avis sur sa pertinence ou sa formulation et à ajouter des sources dans l'article.
Les anecdotes sont destinées à la section « Le Saviez-vous ? » de la page d'accueil de Wikipédia. Elles doivent d'abord être proposées sur la page dédiée.
(ceci est un message automatique du bot GhosterBot le 03 août 2023 à 11:16, sans bot flag)