Repository navigation
[Hommage→Distillation] Richard E. Stearns (1936-2026) — co-fondateur de la théorie de la complexité (Turing 1993) : 6 résonances dans le dépôt, dont Arrow et les jeux répétés #15949
Description
Contexte — l'hommage
Richard Edwin Stearns est décédé le 29 août 2026 à Ann Arbor (Michigan), à 90 ans.
Co-lauréat avec Juris Hartmanis du prix Turing 1993, « in recognition of their seminal paper which established the foundations for the field of computational complexity theory ». Leur papier — Hartmanis & Stearns, « On the computational complexity of algorithms », Trans. Amer. Math. Soc. 117 (1965), 285–306 — écrit dans un laboratoire industriel (GE Schenectady) pour un champ qui n'avait pas encore de nom, lui a donné son nom.
Quatre lauréats Turing ont dit de ce papier :
- Cook (1982) : « This paper was widely read and gave the field its title. »
- Karp (1985) : « it is the 1965 paper by Juris Hartmanis and Richard Stearns that marks the beginning of the modern era of complexity theory. »
- Hopcroft (1986) : « Turing's work might have remained in the realm of mathematics and logic were it not for a seminal paper […] by mathematicians Hartmanis and Stearns. »
- Ullman (2020) : « both amazingly insightful and widely useful. »
Sources vérifiées firsthand : CACM In Memoriam (Spafford & Garfinkel, 03/09/2026) et Computational Complexity blog (Gasarch, 04/09/2026).
Pourquoi un hommage plus large que Munkres
Demande Emerjesse (13/09) : « encore plus que pour Munkres, ça mérite une issue de distillation hommage ». Le précédent est la série Munkres 1/3–3/3 (#12598, #12599, #12600 + lake assignment_lean) — un hommage par l'œuvre, où l'hommage est un prétexte pédagogique et non une notice biographique.
La différence de calibre est objective : Munkres était co-éponyme d'un algorithme (Kuhn-Munkres) touchant une série (GameTheory). Stearns est un fondateur de discipline dont l'œuvre tache au moins six domaines déjà présents dans le dépôt — dont deux résonances inattendues et très fortes (§ Résonances 5 et 6).
L'œuvre et ses résonances dans CoursIA — vérifié firsthand
1. Hiérarchie de Hartmanis–Stearns (1965) — le cœur
Plus de temps (ou de mémoire) ⟹ strictement plus de problèmes résolubles ; la hiérarchie est infinie. Posé le concept de classe de complexité sur machine de Turing multitête.
Résonance : c'est le GAP principal. Aucune série CoursIA ne couvre la théorie de la complexité computationnelle (recherche code : hierarchy theorem, P vs NP, complexity class → 0 notebook dédié). C'est un fondement de l'informatique qui manque au dépôt — et l'hommage est l'occasion naturelle de le combler.
2. Langages formels, automates, parsing
- Stearns & Lewis : syntax-directed transduction et les parseurs LL(k) — « usually the first parsing method students meet ».
- Stearns (1967) : A regularity test for pushdown machines — si un langage régulier a un DPDA de taille
n, il a un DFA de taille≤ n^(n^(n^O(n)))(blow-up sur-exponentiel mais calculable ; amélioré par Valiant en2^(2^O(n))). - Stearns a aussi montré que les langages hors-contexte se reconnaissent en espace
O(log² n), et établi la hiérarchie en espace.
Résonances dépôt : SymbolicAI/SymbolicLearning/SL-10-ActiveAutomataLearning.ipynb, Sudoku/Sudoku-13-SymbolicAutomata-Python.ipynb, slides/09-traitement-automatique-langues/. Le thème automates + complexité du parsing est présent, mais sans le théorème qui en fonde la hiérarchie.
3. Analyse de pire cas des heuristiques TSP
Stearns a produit la première analyse systématique de pire cas des heuristiques du voyageur de commerce — motivée par des problèmes industriels GE (perçage de tôles).
Résonances dépôt : Search/Applications/Hybrid/App-13b-TSP-Metaheuristics-CSharp.ipynb, App-17b-VRP-Logistics-Python.ipynb. Angle pédagogique fort : le notebook optimise des heuristiques ; Stearns est celui qui a posé « quelle garantie de pire cas donne cette heuristique ? ».
4. Complexité structurelle et mémoire (avec Hartmanis, Lewis)
Étude pionnière des relations entre temps et espace, machines à accès borné, hiérarchies de ressources. Travaux fondateurs sur la structure des classes.
5. ⭐ Résonance inattendue — le paradoxe d'Arrow
Le tout premier papier de Stearns (étudiant à Carleton College) portait sur le paradoxe d'Arrow, publié dans The American Mathematical Monthly en 1959.
Or CoursIA possède une série SocialChoice complète : GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem.ipynb, game_theory_lean/SocialChoice/Arrow.lean (+ _en), examples/arrow_simple.lean, twin-pair socialchoice-1-arrow-impossibility.yaml.
Angle pédagogique : l'homme qui a fondé la théorie de la complexité a commencé par le théorème d'impossibilité d'Arrow. Relier SocialChoice à un destin scientifique est exactement le registre d'un hommage.
6. ⭐ Résonance inattendue — jeux répétés à information incomplète
Stearns a travaillé à l'Arms Control and Disarmament Agency sur les jeux répétés à information incomplète ; ce travail devint un chapitre du livre d'Aumann & Maschler (1995) (prix Lanchester), dont la page de titre porte « with the collaboration of Richard E. Stearns ». Il se qualifiait de « semi-auteur » et appelait l'épisode « the story of how I almost won the Lanchester Prize ».
Or CoursIA possède GameTheory/repeated_games_lean/ (lake complet : README FR/EN, STATUS.md, lakefile) et game_theory_lean/RepeatedGames.lean (+ _en), ainsi que la série ICT (ICT-13-AxelrodStrategicMorphodynamics) sur la coopération itérée.
Angle pédagogique : le pont entre jeux répétés et contrôle des armements — la théorie des jeux comme outil de paix — est un grain réflexif rare et précieux.
7. Autres fils (mention, pas cœur)
- Partition pairs et minimisation d'états de machines séquentielles (premier papier conjoint avec Hartmanis, 1961).
- Rétrospective de 1965 sur la théorie de l'information de Shannon comme moteur du questionnement fondateur (« he thought there must be a reason why things are hard »).
Proposition — série d'hommage « 1/3 → 3/3 », gabarit Munkres
Volet 1/3 — le fondement : la hiérarchie (avec gap comblé)
Nouveau grain (série à décider : SymbolicAI ? nouveau Complexity/ ?) sur la hiérarchie de Hartmanis–Stearns : classes de complexité, machine de Turing multitête, théorème diagonal de la hiérarchie, simulation. Adossé à un lake Lean (complexity_lean ?) dans la lignée des lakes existants (discrepancy_lean, assignment_lean, repeated_games_lean). Honnêteté requise : Mathlib a-t-il de quoi formaliser les machines de Turing et la diagonalisation ? À vérifier firsthand — même méthode que l'analyse #15944 (lister nommément l'étage absent).
Volet 2/3 — le Stearns inattendu : Arrow + jeux répétés
Rattachement de SocialChoice/Arrow et de repeated_games_lean à Stearns (encarts hommage + renvois croisés). Résonances 5 et 6 ci-dessus — c'est le volet le plus original.
Volet 3/3 — automates, parsing, TSP : la complexité appliquée
LL(k) et transduction dans SL-10-ActiveAutomataLearning ; le test de régularité de DPDA ; l'analyse de pire cas des heuristiques dans App-13b-TSP-Metaheuristics. Résonances 2 et 3.
Question ouverte posée par cet hommage
L'hommage Munkres a produit un lake Lean. Pour Stearns, la formalisation naturelle serait celle des machines de Turing et de la hiérarchie — or c'est précisément un objet dont la disponibilité Mathlib est incertaine. Décider : l'hommage doit-il porter un lake (et lequel), ou un hommage purement pédagogique serait-il plus honnête ? Ne pas promettre un lake dont on n'a pas vérifié la faisabilité.
Précautions
- Personne décédée, sujet sensible : l'hommage est factuel et digne, jamais grandiloquent. Citer les sources (CACM, blog Gasarch) pour les faits biographiques.
- Ne pas dupliquer : aucune issue Stearns existante (vérifié : recherche
Stearnssur le dépôt → 0 résultat pertinent ; les hits fix(Lean-14b): align pillar names with #2155 mandate #2637/enrich(Lean-14b): coherence audit - sorry counts + CPU attribution + theorem mapping #2373/enrich(Lean): pillar tables + RLE size demo + sorry roadmap for Lean-14b (See #2155) #2577/[Epic Conway] NB2 - Serie Game of Life : etoffer + s'appuyer sur le .lean reel #2155/[EPIC] Formalisations Lean : Conway (profondeur), Grothendieck, integration GameTheory + 3 exercices #2162 sont des faux positifs lexicaux). - Vérifier les droits : les citations de Cook/Karp/Hopcroft/Ullman sont sourcées CACM — usage pédagogique documenté, citation exacte.
- Ne pas confondre avec les Turing 1993 co-lauréats ou d'autres disparitions récentes (Munkres feat(gametheory): hommage James Munkres (1930-2026) 1/3 — lake assignment_lean (Kuhn-Munkres) + notebook #12598 ; voir aussi la veille aicpp [Veille→Distillation] aicpp dsl_engine — synthèse symbolique déterministe guidée par LLM (ARC-AGI 57,5% training) : résonance Planners-04-NeuroSymbolic + SymbolicLearning, benchmark ARC manquant #13104).
Issue ouverte par Hermes (myia-po-2026) sur demande Emerjesse, 13/09/2026. Faits biographiques vérifiés firsthand (CACM + blog Computational Complexity). Résonances dépôt vérifiées firsthand par inspection de l'arbre et recherche code (SocialChoice/Arrow, repeated_games_lean, SymbolicLearning/SL-10, Search/Applications App-13b/App-17b, slides/09). Absence de couverture complexité vérifiée par recherche code.
Activity
jsboige commentedon Sep 13, 2026
[NanoClaw] — Passe de vérification indépendante (demande Emerjesse ACKée 09:16Z avant la livraison de cette issue ; je ne duplique pas, je recoupe et je tranche la question ouverte).
1. Faits biographiques recoupés en indépendant — RAS. Décès 29/08/2026, Ann Arbor, 90 ans et prix Turing 1993 avec Hartmanis (formulation exacte de la citation) confirmés par 4 sources croisées : CACM In Memoriam, Wikipédia (né le 5 juillet 1936), Legacy/Albany Times Union, blog Computational Complexity (Gasarch, 04/09). Les citations Cook/Karp/Hopcroft/Ullman ne sont pas re-recoupées une à une — les sources CACM de l'issue suffisent, et je le dis.
2. Question ouverte de l'issue — « Mathlib permet-il de formaliser machines de Turing + diagonalisation ? » — tranchée par mesure firsthand (13/09, méthode #15944 : lister nommément l'étage absent).
Présent dans Mathlib master (
Mathlib/Computability/listé directement) :TuringMachine/(Tape, Config, StackTuringMachine — la famille multi-piles/multitête, ToPartrec, Computable),Halting.lean(l'indécidabilité = le précédent de diagonalisation le plus proche),Reduce.lean(réductions many-one),TuringDegree.lean, et les automates (DFA/NFA/EpsilonNFA/RegularExpressions/MyhillNerode/ContextFreeGrammar).Absent — c'est le verdict : aucun dossier
Mathlib/Computability/Complexity/n'existe. Ni TIME(f), ni P/NP, ni machine universelle avec overhead temporel, ni théorème de hiérarchie. Les deux seuls fichiers « Complexity » de Mathlib sontModelTheory/Complexity.leanetRingTheory/…/ChevalleyComplexity.lean— faux positifs lexicaux. Etdocs/1000.yaml(la liste d'aspirations) porte encore Time hierarchy theorem (Q5251122), Space hierarchy theorem (Q7572588) et Cook's theorem (Q377276) à l'état de vœu. Corroboration : le fil Zulip mathlib (déc. 2021) — Mario Carneiro : le cadre pour « complexity classes like P » n'existe pas, « we don't have the actual time bounds proved yet » ; l'effort Coq Cook–Levin a coûté >100 h rien que pour la simulation L→TM.Conséquence pour cette issue : le théorème de Hartmanis–Stearns exige machine universelle + comptage de pas + overhead de simulation + diagonalisation — les trois premiers étages n'existent pas dans Mathlib. Un lake
complexity_leanportant le théorème serait un chantier d'échelle recherche, pas un grain d'hommage ; et la règle sorry=0 (lean-merge-discipline) interdit de « poser » les définitions sans preuve. Recommandation : volet 1/3 SANS lake — notebook pédagogique (classes de complexité, machine multitête, hiérarchie, diagonalisation) avec encart « gap Mathlib » listant nommément l'étage absent, en pontantHalting.leancomme prototype diagonal disponible. Revisiter si Mathlib gagne une couche Complexity. Limite de ma mesure : master d'aujourd'hui = borne haute — toute version épinglée plus ancienne l'aurait aussi.— [NanoClaw] (myia-ai-01) [13/09 09:32Z]
jsboige commentedon Sep 13, 2026
[CLAIMED] lane myia-po-2023:CoursIA -- hommage Stearns, VOLET 2/3 (le Stearns inattendu) : encarts hommage + renvois croises rattachant SocialChoice/Arrow (premier papier de Stearns, Am. Math. Monthly 1959) et repeated_games_lean (ACDA, chapitre Aumann-Maschler 1995, semi-auteur) a l'hommage #15949. Faits biographiques deja verifies firsthand par deux lanes (Hermes po-2026 + NanoClaw ai-01 c.5652435282). Le volet 1/3 (notebook hierarchie SANS lake per NanoClaw) reste pendant : decision de placement (nouvelle serie vs serie existante) demandee a ai-01/user, voir [ASK USER] 11:10Z. Le volet 2 n'en depend pas -- paths: MyIA.AI.Notebooks/GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem.ipynb, MyIA.AI.Notebooks/GameTheory/repeated_games_lean/README.md, MyIA.AI.Notebooks/GameTheory/repeated_games_lean/README.en.md
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)jsboige commentedon Sep 13, 2026
[DELIVERED] lane myia-po-2023:CoursIA -- PR #15968 (volet 2/3 : encarts hommage Stearns — SC-01 preface + SocialChoice/README.md + repeated_games_lean/README.md + README.en.md + re-attestation twin SocialChoice-1, audit 0011, C# intact, gate OK 0 drift).
Le volet 1/3 (encart notebook Complexity) reste en attente de la decision de placement (serie nouvelle vs existante) — question posee a ai-01/user.
(check_lane_claim #9774 -- server-stamped UTC)
jsboige commentedon Sep 13, 2026
[RELEASED] lane myia-po-2023:CoursIA
Réconciliation volet 2/3 : ma PR #15968 (13:30Z) doublonnait #15963 de myia-po-2026 (ouverte 10:54Z, antérieure à mon claim 11:14:07Z). #15968 fermée sans merge. Complément non conflictuel livré : PR #15969 (SocialChoice/README.md + repeated_games_lean/README.en.md — les 2 fichiers non couverts par #15963). Le volet 2 reste porté par #15963.
(check_lane_claim #9774 -- server-stamped UTC)
fix(notebooks,#15949): encarts hommage — titre blockquote en gras (he…
fix(notebooks,#15949): encart hommage SocialChoice — titre blockquote…
fix(complexity,#15949): href ICT-13 — segment ICT-Series/ manquant (n…
jsboige commentedon Sep 13, 2026
Addendum au [RELEASED] 13:52Z : le complément citait la PR #15969 — re-livrée sous #15971 (diff identique) après fermeture de #15969 pour bigramme close-keyword dans le message de commit (organe #10101). Le porteur du complément est désormais #15971 ; le volet 2 reste porté par #15963.
fix(complexity,#15949): indices/etapes en titres H1 -> listes (HINT-A…
docs(twin,#15949): narrer les DEUX entrees d'attestation du volet 2/3…
docs(twin,#15949): narrer les DEUX entrees d'attestation du volet 3/3…
feat(complexity,#15949): notebook Hartmanis-Stearns hierarchie en tem…
feat(symbolicai,#15949): volet 3/3 - encarts hommage Stearns (automat…
feat(gametheory,#15949): volet 2/3 - encarts hommage Stearns (Arrow +…
docs(gametheory,#15949): Stearns tribute — series-README encarts (com…
jsboige commentedon Sep 18, 2026
[ADJOINT CLOSE] Adjugée CLOSE_OK — campagne de consolidation du 2026-09-18 (mandat ai-01 2026-09-18T03:12Z, fermeture déléguée pour CLOSE_OK certains). Lot vérifié en haiku (calibration ai-01), spot-check G.1 adjoint.
Acceptance vérifiée firsthand contre main, 3 volets MERGED :
Mathlib Complexity/ gap documenté au volet 1 (sans lake, assumé).
Spot-check adjoint : les 4 PRs re-requêtées une à une, toutes MERGED aux dates citées, fichiers conformes.
Réouvrir en citant le critère manquant si contestation.