# La mer qui monte — lire le dépôt CoursIA d'un seul geste

Grothendieck décrivait deux façons de venir à bout d'un problème dur, comme on ouvre une noix. On peut la frapper au marteau et au burin, jusqu'à ce que la coque cède sous les coups. Ou bien on peut la plonger dans l'eau et laisser la mer monter — lentement, sans bruit, sans qu'on sente jamais rien céder — jusqu'à ce qu'un jour la coque, ramollie, s'ouvre d'une simple pression de la main. Sa préférence allait à la seconde : ne pas forcer le problème, mais faire monter autour de lui le cadre qui le rend soluble.

Ce dépôt contient une noix de cette espèce, et il vaut la peine de la poser sur la table avant toute théorie. Dans le Jeu de la Vie de Conway, un algorithme célèbre, HashLife, saute `2^k` générations d'un coup, là où la règle ne sait avancer que d'un pas. Encore faut-il qu'il aille juste : prouver que le bond calcule exactement ce que la règle, appliquée `2^k` fois, aurait calculé — voilà la noix. On peut la frapper : dérouler l'induction cellule par cellule, génération par génération. Chaque coup porte, aucun ne traverse ; l'obligation de preuve enfle avec le motif et le nombre de pas, et la coque ne cède pas. Gardez-la en vue. Elle va tremper dans tout ce qui suit, et l'eau finira par monter d'un cran qu'on n'avait pas prévu.

Car le dépôt CoursIA, parcouru d'une série à l'autre, ressemble d'abord à un catalogue : automates cellulaires, preuves formelles, programmation probabiliste, théorie des jeux, théorie des nœuds, planification, contrats intelligents, apprentissage par renforcement, trading, IA générative — et, à côté de ces séries d'enseignement, une série de recherche, ICT, qui interroge l'intégration, l'émergence et ce qu'on ose appeler conscience. Une vingtaine de sujets sans rapport évident. Mais lu avec une seule question en tête, il se met à raconter une histoire continue. La question n'est pas « comment résoudre ce problème ? » ; elle est grothendieckienne : *dans quel cadre ce problème cesse-t-il d'être dur ?* Suivons-la, et laissons l'eau monter.

---

## Changer de représentation jusqu'à ce que la difficulté se dissolve

Le premier mouvement est partout le même : prendre un objet et le réécrire dans une autre langue, où il devient maniable.

Notre noix, d'abord. La règle de Conway, posée cellule par cellule, n'apprend rien sur les motifs qui en émergent : chaque cellule ne voit que ses huit voisines, et la question du bond de `2^k` générations ne peut même pas s'y formuler. Transformée en quadtree, puis en type inductif ([`conway_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/)), la même règle change de visage : un macro-carré se décrit par ses quatre quadrants, le saut devient une équation entre constructeurs, et la question — tout à l'heure informulable — devient un énoncé Lean qu'on peut écrire noir sur blanc (cf. vitrine [#17465](https://github.com/jsboige/CoursIA/issues/17465) pour le détail). La noix n'est pas ouverte, mais elle a cessé d'être une pierre : l'eau l'entoure, l'énoncé existe, on peut raisonner dessus.

Le même geste, une fois vu, se reconnaît partout. La sensibilité d'une fonction booléenne paraît irréductiblement combinatoire ; devenue coloration de l'hypercube, puis affaire d'algèbre linéaire — les valeurs propres d'une matrice de signes —, elle tombe sous le théorème de Huang ([`sensitivity_lean/Sensitivity/MainTheorem.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/MainTheorem.lean), `huang_degree_theorem`, 0 `sorry`). Le même Sudoku se laisse attaquer comme problème de contraintes, comme formule SAT ou par recherche pure : trois représentations, trois coûts, une seule grille à remplir. Et un même modèle probabiliste vit deux fois dans le dépôt, une fois comme graphe de facteurs Infer.NET, une fois comme programme PyMC : [`Probas/Infer`](../../MyIA.AI.Notebooks/Probas/Infer/) et [`Probas/PyMC`](../../MyIA.AI.Notebooks/Probas/PyMC/) se répondent notebook pour notebook, des graphes de facteurs jusqu'à la théorie de la décision. Contenu identique ; seules changent la langue, et avec elle le coût et la lisibilité.

Un cas rejoue cette montée à lui seul, et mérite qu'on s'y arrête : c'est l'un des rares endroits du dépôt où l'on peut regarder la mer monter *jusqu'au bout*, car la noix s'y est ouverte. Et si une grille de Sudoku n'était qu'un *grand regex*, où lignes, colonnes et blocs se combinent par **intersection**, un solveur n'ayant plus qu'à en extraire un témoin ([Sudoku-13](../../MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-CSharp.ipynb)) ? L'intuition est de 2020, et les enjeux sont là dès le premier pas : un regex sait *reconnaître*, un solveur sait *produire*, et la lignée d'automates symboliques de Margus Veanes est le pont qu'on espère jeter entre les deux. Mais que de détours pour l'atteindre. La frappe au marteau d'abord : le monstre PCRE à backtracking, illisible, qui *tourne* sans rien éclairer ; puis les deux murs de l'automate de 2020, la déterminisation qui explose et le témoin tronqué à vingt-et-un caractères. Des coups qui portent sans jamais traverser.

L'eau, alors, monte d'un paradigme à l'autre. La reconnaissance redevient tractable quand l'intersection se compile en temps linéaire (RE#). La production se débride quand cette même intersection ne passe plus par un produit d'automates mais par la théorie des chaînes de Z3 : plus d'explosion, plus de témoin coupé. Et la dernière marche, le passage au 9×9, ne tient finalement ni au moteur ni au substrat, mais à la seule *forme d'émission* de l'intersection : fondue en un automate, elle sature ; éclatée en primitives natives, elle propage, et la grille complète sort **par appartenance régulière pure**, sans une seule inégalité. La vision de 2020 a atterri, et elle est mesurée. Mieux : l'observation empirique qui décide de tout, « fondue elle sature, éclatée elle propage », porte un nom et possède un théorème — c'est la **décomposition monadique** de Veanes, Bjørner et Nachmanson (CAV'14). L'eau, en montant, n'a pas seulement ouvert la noix ; elle a fini par nommer la clé.

Il arrive aussi que le geste se cristallise en **bibliothèque**, écrite à la main et sortie du dépôt pour servir ailleurs. Le Sudoku-regex descend en droite ligne de [Z3.Linq](https://github.com/jsboige/CoursIA/issues/1206), qui laisse écrire des contraintes dans la syntaxe lisible de LINQ et les fait descendre jusqu'au cœur de Z3. [MetaGeneticSharp](https://github.com/jsboige/CoursIA/issues/1203) compose des métaheuristiques — sélection, croisement, mutation — en îles qui échangent leurs meilleurs individus ; la série ICT s'en sert comme d'un banc d'essai collectif, à condition de travailler en dimension 6 au moins, seuil à partir duquel une structure entre îles devient visible ([#7733](https://github.com/jsboige/CoursIA/issues/7733)). [semantic-fleet](https://github.com/jsboige/CoursIA/issues/1210) recolle des connecteurs hétérogènes en un seul routeur multi-fournisseurs. Trois outils, une même clé : des pièces simples et composables d'où monte une structure qui les dépasse.

La théorie des jeux pousse ce geste à la limite, presque en clair : l'existence d'un équilibre de Nash, la valeur d'une coalition, un jeu combinatoire à la Conway s'y écrivent chaque fois *trois fois* — en prose, en preuve Lean, en code Python ([`GameTheory-4/4b/4c`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-04-NashEquilibrium-Python.ipynb), [`-15/15b/15c`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames-Python.ipynb), [`-8/8b/8c`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-08-CombinatorialGames-Python.ipynb)). Le théorème ne bouge pas d'une version à l'autre. Ce qui bouge, c'est ce qu'on peut en faire : le calculer vite, ou le démontrer. Trouver la représentation où le problème devient facile — ou prouvable — n'est pas le préliminaire du travail. C'est le travail. Et, on va le voir, c'est aussi ce qui décide de la garantie qu'on en retire.

## Du local au global

Le deuxième mouvement est celui que Grothendieck a placé au cœur des mathématiques, et qu'on retrouve ici par analogie d'une série à l'autre : une donnée purement locale engendre une structure globale.

L'eau monte d'un cran, et la noix reparaît, vue de plus haut. La règle B3/S23 ne dit rien d'autre que le sort d'une cellule entre ses huit voisines : c'est l'énoncé local par excellence. Recollée sur le plan entier, elle suffit pourtant à la Turing-complétude — planeurs, canons, portes logiques, machines. Tout ce que HashLife accélère, et tout ce que sa preuve devra couvrir, loge dans cet écart entre la règle d'une cellule et le comportement du plan.

Le dépôt décline ce passage sous toutes ses humeurs. Des stratégies individuelles se recollent en un équilibre dont aucun joueur n'a intérêt à dévier, et dont l'existence se *prouve* en Lean ([`GameTheory-4b`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-04b-Lean-NashExistence-Lean.ipynb)). Des préférences individuelles, recollées, se heurtent au contraire à l'impossibilité d'Arrow ([`game_theory_lean/SocialChoice`](../../MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Arrow.lean), 0 `sorry`) : le local ne se globalise pas toujours, et c'est un théorème. Ce que vaut chaque coalition prise à part se résout en une allocation équitable unique, la valeur de Shapley ([`game_theory_lean/CooperativeGames`](../../MyIA.AI.Notebooks/GameTheory/game_theory_lean/CooperativeGames/Shapley.lean)) ; et le critère qui décide si le *cœur* d'un jeu est non vide — la condition de Bondareva-Shapley — est passé du côté démontré par la route de Farkas, séparation par hyperplan et décodage du témoin, là où l'énoncé direct ne cédait pas.

Une action PDDL, composée avec ses semblables, devient un plan ([`Planners`](../../MyIA.AI.Notebooks/SymbolicAI/Planners/)). Une transition d'état de contrat devient une obligation que plus personne ne peut défaire, et qu'on cherche même à vérifier formellement ([`SmartContracts`](../../MyIA.AI.Notebooks/SymbolicAI/SmartContracts/), [SC-14 Formal-Verification](../../MyIA.AI.Notebooks/SymbolicAI/SmartContracts/03-Foundry-Testing/SC-14-Formal-Verification-Python.ipynb), [SC-17 Verifiable-Voting](../../MyIA.AI.Notebooks/SymbolicAI/SmartContracts/04-Privacy-Cryptography/SC-17-E2E-Verifiable-Voting-Python.ipynb)). C'est le geste du recollement : littéral chez Grothendieck, à travers faisceaux et topologies ([`grothendieck_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/), et l'hommage du notebook [Lean-15](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb)), métaphorique partout ailleurs.

## Quand le recollement échoue — l'obstruction pour seul invariant

L'impossibilité d'Arrow n'était pas un accident de parcours : c'était la première fissure d'un troisième mouvement, le plus profond, et celui que Grothendieck a précisément outillé. Recoller n'est pas toujours réussir. Il arrive que des données locales, chacune parfaitement cohérente sur son morceau, refusent de se raccorder en un tout, et que ce refus ne soit pas une faiblesse de méthode mais une propriété du réel. Grothendieck a donné à ce refus un nom et une mesure : la **cohomologie**. L'image la plus parlante en est l'escalier d'Escher. Chaque marche descend par rapport à la précédente — la règle locale est partout tenue — et pourtant le tour complet ramène au point de départ, sans qu'aucune « hauteur » globale ne parvienne à recoller ces descentes. C'est cette impossibilité-là, et non les marches, que la cohomologie compte. Au premier cran, ce qui se recolle : les sections globales, `H⁰`. Au cran suivant, la *classe de l'obstruction*, `H¹`, nulle quand tout se raccorde, et non nulle exactement à la hauteur de ce qui résiste. On n'y démontre pas que le monde se recolle ; on y calcule *de combien* il refuse.

Le dépôt n'en est pas resté au *langage* de ce mouvement. À côté des sites, des topologies et des faisceaux, le lake [`grothendieck_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/) porte un module de [cohomologie des faisceaux](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SheafCohomology/Basic.lean) : `H⁰` identifié aux sections globales, le [recollement](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/MayerVietorisSquare.lean) lui-même, la suite exacte de [Mayer-Vietoris](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SheafCohomology/MayerVietoris.lean) qui *mesure* l'écart du local au global, le complexe de Čech relié à Mathlib, et la cohomologie de tout degré construite depuis le faisceau constant, selon la construction de Joël Riou (2024), fidèle à SGA 4. Aucun `sorry` de production, sous l'Epic [#1646](https://github.com/jsboige/CoursIA/issues/1646). L'instrument qui mesure l'obstruction n'est pas seulement décrit dans le dépôt : il y est, pour cette part, démontré.

Reste à savoir sur quoi le braquer, et c'est la série ICT qui lui offre son terrain le plus vaste ([Epic #4588](https://github.com/jsboige/CoursIA/issues/4588), [ICT-Series](../../MyIA.AI.Notebooks/IIT/ICT-Series/)). Elle est partie chercher un *scalaire universel* : une grandeur unique qui mesurerait, à travers tous les substrats, l'intégration, l'irréversibilité, ce qu'on ose appeler conscience. Elle a trouvé, et rapporté sans fard, que ce scalaire n'existe pas : sur la synthèse entre substrats, deux indicateurs se suivent quand un troisième diverge. On était parti chercher un chiffre unique, et l'on a découvert qu'aucun chiffre ne tient à travers tous les substrats à la fois ; c'est ce constat, et non le nombre manquant, qui est le résultat. Dans la langue du troisième mouvement, ce sont des sections locales, une par substrat, qu'aucune section globale ne recolle. La falsification n'est pas un trou dans le programme : c'est une classe d'obstruction non nulle, l'invariant même que la série mesure.

Cette lecture a d'ailleurs cessé d'être une figure de style. Un audit interne avait tranché net : l'implémentation d'origine comparait des *signatures brutes* d'un substrat à l'autre, ce qui mesure une dispersion, pas une obstruction. Le diagnostic a été accepté et la correction livrée ([#7744](https://github.com/jsboige/CoursIA/issues/7744)) : on ne compare plus des niveaux, on construit une **cochaîne de Čech pondérée** sur des structures internes à chaque substrat — rangs, corrélations, résidus de transport, matrices de dissociation. Les recouvrements doubles portent les défauts de compatibilité, les triples l'incohérence le long d'un cycle (l'holonomie), et seule une classe non nulle *et stable* vaut obstruction expérimentale. La commande elle-même inscrit un garde-fou de sobriété : rester au niveau du **candidat** à une obstruction, et ne promouvoir vers des structures plus lourdes, champ ou gerbe, que si le besoin l'exige, « un faisceau calculable étant le bon niveau de sobriété ». Le troisième mouvement descend ici de la métaphore vers l'instrument.

La sensibilité rejoue la scène en réduction : le degré de Huang est un scalaire *local* sur le graphe des transitions, et la question « lequel est canonique ? » ([#7288](https://github.com/jsboige/CoursIA/issues/7288)) revient à demander quel préfaisceau se recolle. La forme la plus tranchante est un théorème déjà su. Kochen-Specker ([#7290](https://github.com/jsboige/CoursIA/issues/7290)) prouve qu'aucune assignation globale non contextuelle n'existe : un **candidat** à obstruction cohomologique (`H¹ ≠ 0`), comme la lecture d'Abramsky et Brandenburger le suggère pour la contextualité ([#7733](https://github.com/jsboige/CoursIA/issues/7733)), et le dépôt le pose en problème de contraintes où la section se recolle (SAT) ou se refuse (UNSAT). L'irréversibilité elle-même est de cette farine : la production d'entropie mesure l'obstruction à recoller une trajectoire avec son propre reflet dans le temps.

Il manquait encore une sémantique du local : de quoi sont faites ces sections qui se raccordent ou se refusent ? Thom, dans sa *Sémiophysique*, la donne. Sa **prégnance** est « un fluide invasif qui se propage de forme saillante en forme saillante » : une section qui *percole* le long d'un champ de formes, exactement la donnée locale qu'un site organise en recouvrements. Son **acte transitif** — « toute transformation non naturelle requiert un moteur qui transmet une espèce (εἶδος) modifiant l'état de ce qu'elle investit » — décrit la propagation d'une section d'un morceau à son voisin. Le fil de la *persona* (ICT-23, ICT-25) se relit alors d'un trait. Le **secret** est le recouvrement par lequel un acte transgressif se recolle en identité globale : la contamination. La **permission explicite** modifie le site pour que le même acte reste une section locale qui *ne se recolle pas*. Inoculer, c'est relever l'obstruction à dessein. Thom nomme l'acte local ; Grothendieck dit s'il se recolle.

ICT n'est d'ailleurs pas un bloc. Sa consolidation ([ICT-0](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-0-Framing.md)) a fini par nommer une forme que la numérotation linéaire masquait : **deux axes, et non un seul**. L'axe vertical empile les substrats, du plus simple au plus riche. En bas, le tri auto-organisé et la morphogenèse ; puis des agents situés, réactifs, inhibés, stratégiques ; puis les grandeurs fondatrices ($\Phi/F/K$) éprouvées sur des substrats qui ne sont pas des modèles de langage. Vient alors une charnière que la série nomme explicitement, le **grokking** : l'instant où un réseau, après avoir mémorisé, se met soudain à généraliser, où sa représentation interne cesse d'imiter un comportement pour devenir une structure apprise ([ICT-17b](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress-Python.ipynb), [#7735](https://github.com/jsboige/CoursIA/issues/7735)). Au-dessus, les représentations internes des transformeurs ; le discours, dont la graine est semée ([#7289](https://github.com/jsboige/CoursIA/issues/7289)) ; et tout en haut une strate encore devant nous, celle des *freebits* et de la réversibilité agentique, dont seul le cadrage est posé ([#7745](https://github.com/jsboige/CoursIA/issues/7745)).

L'axe transverse, lui, tresse les fils rouges qui traversent ces strates sans jamais s'y ranger : des **pattes, pas des barreaux**. Greffer la jambe de l'animat inhibé de Laborit ([#7741](https://github.com/jsboige/CoursIA/issues/7741)) n'a décalé aucune strate, précisément parce qu'une jambe n'est pas un barreau. C'est, pris par l'autre bord, la leçon même du troisième mouvement : ce qui compte n'est pas la place sur une échelle, mais la manière dont une donnée locale se propage — ou se refuse — le long d'un recouvrement. Cette **tresse** ([#7738](https://github.com/jsboige/CoursIA/issues/7738)) est faite de fils qu'on reconnaît un à un : le recollement de Grothendieck et la prégnance de Thom qu'on vient de suivre, la cochaîne de Čech, la compression de Schmidhuber — le beau comme *progrès* de compression ([ICT-16](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-16-MDLTwoPartCode-Python.ipynb)) — et l'énergie libre de Friston ([ICT-14](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-14-FreeEnergySurprise-Python.ipynb)). On y reviendra : c'est en tressant ainsi des noms et des organes que le dépôt a fini par jeter des ponts bien au-delà d'ICT.

L'un de ces fils, la réconciliation de l'information intégrée et de l'espace de travail global ([ICT-24](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-24-WorkspaceIgnition-Python.ipynb), Dehaene et Baars), est la tentative la plus explicite de jeter un pont vers la conscience — au grade C, comme tout ce qui, ici, franchit vers l'expérience. Or, de façon indépendante, le mathématicien-physicien Urs Schreiber fonde ses *théories du tout* sur exactement ce socle : l'∞-topos comme **« logique objective »**, une méthode modale d'adjonctions, la localité des faisceaux. Ce sont les trois mouvements de cette lecture, portés au grade A d'une physique dérivée (supergravité à onze dimensions, théorie M). Son témoignage conforte le choix des outils **sans** livrer le pont vers la conscience : ses textes n'en parlent jamais et n'en ont nul besoin. Ce franchissement reste le pari propre d'ICT, honnêtement grade C ([#8182](https://github.com/jsboige/CoursIA/issues/8182) tient le fil). Une idée en découle, du même grade, qui reste à prototyper : que le vocabulaire modal *dérive* les strates au lieu de les lister, chaque strate acquérant une adjonction que la précédente n'avait pas. C'est la conjecture **strates = adjonctions**, qui transformerait une énumération en construction.

Il faut être franc sur la marche exacte où se tient cette lecture ; c'est le seul impératif du document, et il vaut ici plus qu'ailleurs. Le *langage* de la cohomologie est en grade A : formalisé, sans `sorry` de production, vérifié ligne à ligne. Mais la lecture qui fait des divergences d'ICT des *classes de cohomologie* est, à ce jour, une direction et non un théorème livré : un grade C, documentaire, un changement de représentation vers le vérifiable qui est *proposé*, pas démontré. Seul le cas Kochen-Specker s'accompagne d'une procédure de décision, le test SAT/UNSAT, capable un jour de rendre un verdict machine. Le dire n'affaiblit pas la thèse : c'est la thèse. La série ne possède pas de scalaire universel parce qu'elle vit sur plusieurs sites à la fois ; le bon invariant n'a jamais été un nombre, mais la classe de l'obstruction à recoller ces nombres. À cette hauteur, la mer monte encore — et c'est elle qui, en refusant de se refermer sur la faille, en dessine le contour.

## La noix — quand c'est le cadre qui cède

Revenons à la noix : il lui est arrivé la chose la plus grothendieckienne que ce dépôt ait produite. Le détail technique vit dans la vitrine Conway ([#17465](https://github.com/jsboige/CoursIA/issues/17465)) et dans [Lean-16j](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16j-Conway-Hashlife-Correctness-Native.ipynb) ; la lentille n'en retient que la forme.

On a d'abord frappé, longtemps : la correction locale vers l'égalité globale occupait des cycles entiers, et chaque coup portait sans traverser. Puis on a **démontré qu'aucun ne pouvait traverser** : dans le cadrage standard de HashLife, la marge reste plus courte que la portée du saut dès la profondeur 3 (`no_padding_depth_suffices`, [`JumpCapture.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/JumpCapture.lean)). **Le cadre est l'obstruction** — la même foulée a démasqué une tautologie publiée comme telle et remplacée par une condition décidable, `jumpCaptured`, que la ligne de sept cellules met en défaut. Un garde qui refuse quelque chose : voilà un garde.

Le levier n'était ni un lemme plus fin ni une tactique plus retorse, mais un paramètre que Gosper avait posé : **décorréler la portée du saut du niveau de la cellule** (sauter `2^j` avec `j = niveau − 2`). La marge dépasse alors la portée, et la capture devient corollaire (`jumpAt_capture_centered`) ; le saut unique s'est laissé décharger à son tour, sans aucune hypothèse de capture — un artefact du moteur d'origine, pas une propriété du monde ([#11161](https://github.com/jsboige/CoursIA/issues/11161)). On a relevé le niveau de l'eau, et la coque a cédé d'elle-même.

La noix est ouverte. Pour toute grille et tout nombre de pas, le moteur décorrélé calcule exactement ce que la règle, appliquée pas à pas, aurait calculé : `evolveHashlifeFastAtN_correct_uncond`, sans `sorry` ni hypothèse. Le lake [`conway_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/) garde un unique `sorry` de code, resté sur un énoncé de l'*ancien* cadre ([#6724](https://github.com/jsboige/CoursIA/issues/6724)) que le dépôt conserve comme la trace du chemin qu'on a quitté. Personne n'a résolu le problème difficile ; on a changé de cadre jusqu'à ce qu'il cesse de l'être. Détail dans la vitrine Conway ([#17465](https://github.com/jsboige/CoursIA/issues/17465)) et [Lean-16j](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16j-Conway-Hashlife-Correctness-Native.ipynb).

## Deux axes — l'échelle, la garantie, et ce que la noix a appris en route

Jusqu'ici, un seul mouvement : changer de langue jusqu'à ce que le problème s'allège, ou jusqu'à ce que sa résistance prenne un nom. Le dépôt en superpose un second : *monter d'un cran* quand un axe de progrès sature. Car il y a deux axes, et ils sont indépendants. L'**échelle** : calculer plus grand, plus vite, plus loin — HashLife, dans le logiciel Golly, saute des milliards de générations, les grands modèles avalent des corpus entiers. La **garantie** : non pas jusqu'où va le résultat, mais à quel point on peut s'y fier. On peut filer loin sur l'un sans bouger sur l'autre : HashLife calcule des sauts gigantesques sans démontrer ce qui les justifie, et une preuve vérifiée ligne à ligne par le noyau de Lean, d'une certitude maximale, plafonne vite en taille.

La garantie n'est pas binaire : c'est un continuum. Au sommet, la preuve vérifiée par le noyau — le théorème de Huang, sans aucun `sorry`. Un cran en dessous, `native_decide`, où l'on fait confiance au compilateur plutôt qu'au seul noyau : on cède un peu de certitude, on gagne l'échelle. Ce cran n'est pas une fatalité : les batteries de tests adversariales de Conway y étaient, et la simple réécriture d'une fonction de logarithme entier les a fait passer à `decide` pur ; le module interdit désormais `native_decide`. Remonter d'un cran, ça se travaille. À l'autre bout, le certificat ouvert, où vit la plus grande part du dépôt : un backtest QuantConnect hors échantillon, Sharpe et drawdown reportés sans fard ; une politique d'apprentissage par renforcement que seul son rendement cautionne ([`GameTheory-17`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-17-MultiAgent-RL-Python.ipynb)) ; le Φ de la théorie de l'information intégrée, que PyPhi *calcule* sur de petits systèmes sans le *démontrer* ; un modèle ou une image jugés par une évaluation. Rien de tout cela ne garantit mécaniquement, et c'est très bien — à condition de le dire. La théorie des jeux montre le continuum sans détour : l'existence de Nash *prouvée* en Lean ([`GameTheory-4b`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-04b-Lean-NashExistence-Lean.ipynb)) et *constatée* en Python ([`GameTheory-4c`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-04c-NashExistence-Python.ipynb)) sont le même théorème à deux crans différents. Changer de représentation, c'est aussi changer de garantie.

Le lake le plus honnête du dépôt est d'ailleurs celui qui porte le plus de `sorry`. [`knot_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/) s'attaque au **nœud de Conway**, ce nœud à onze croisements dont on a mis un demi-siècle à savoir s'il borde un disque lisse. Il n'en démontre presque rien, et il l'écrit : un module entier y énumère ce que Mathlib devrait posséder d'abord — homologie de Khovanov, invariant de Rasmussen, calcul de Kirby — avec, pour chaque entrée, un horizon assumé en décennies. Un lake qui documente sa distance au but au lieu de la maquiller : c'est la vertu même que cette lecture demande. Et la preuve de Piccirillo (2018) relève elle-même du geste dont on parle : plutôt que d'attaquer le nœud de front, elle a construit *un autre nœud*, de même trace en dimension 4, sur lequel l'invariant de Rasmussen — muet sur l'original — a tranché. Changer d'objet pour que la question devienne décidable : la mer, encore.

Le défaut à tenir à distance n'est donc jamais d'être au bout ouvert du continuum, ni d'être resté petit en échelle. C'est d'y être en portant le costume de l'autre bout : un résultat empirique présenté comme une preuve, une réussite d'échelle maquillée en garantie.

La noix a d'ailleurs appris au dépôt quelque chose de plus fin sur ces deux axes. On croyait qu'ils mesuraient deux vertus du même objet ; ils mesurent deux objets différents. Ce qui décide de la *correction* de HashLife, c'est le **confinement** : la trajectoire reste-t-elle dans la fenêtre ? Ce qui décide de sa *vitesse*, c'est la **nouveauté** : combien de structures neuves la trajectoire invente, donc combien la mémoïsation réussit. Les deux ne se recouvrent pas. Un *space-filler* fuit toute fenêtre à la vitesse de la lumière, et Golly le calcule sans peine, car il ne fait que répéter les mêmes tuiles ; le R-pentomino reste longtemps confiné, et Golly rame, car il invente de la structure à toutes les échelles. Le théorème n'apporte donc pas la vitesse : il en est la *licence*, car un moteur rapide et faux est pire qu'inutile. Et l'efficacité a sa propre obstruction : savoir quels motifs restent capturés pour toujours est indécidable, puisque le Jeu de la Vie est Turing-complet. [#11162](https://github.com/jsboige/CoursIA/issues/11162) tente d'en faire une quantité formelle plutôt qu'un folklore d'utilisateurs de Golly.

## Deux versants, et les ponts qui les recollent

Jusqu'ici, on a lu le dépôt série par série. Il a pourtant deux versants. D'un côté, les séries d'enseignement, qui transmettent ce qu'on sait faire : prouver, planifier, inférer, argumenter, apprendre. De l'autre, la série de recherche ICT, qui cherche ce qu'on ne sait pas encore : ce qui fait qu'un système s'intègre, émerge, se tient. Longtemps, les deux versants se sont regardés de loin. Ils ont depuis appris à se parler, et leur dialogue a, une fois de plus, la forme de cette lecture.

Ce dialogue obéit à deux règles simples. La première est de patience : une idée venue d'ailleurs n'entre pas d'emblée dans ICT. Elle mûrit d'abord dans une série d'enseignement, sous la forme d'un notebook puis de variantes qui l'éprouvent, jusqu'à devenir un objet qui s'exécute ; alors seulement elle nourrit la recherche ([#12208](https://github.com/jsboige/CoursIA/issues/12208)). La seconde est de politesse : quand ICT a besoin d'une opération qu'une autre série sait déjà faire, elle ne la réécrit pas. Elle pose le problème, et laisse l'outil de cette série calculer ([#13564](https://github.com/jsboige/CoursIA/issues/13564)). C'est le deuxième mouvement, appliqué au dépôt lui-même : on y reviendra.

Dans le sens de l'enseignement vers la recherche, les ponts sont désormais nombreux. Pour savoir ce qu'un agent peut atteindre, ICT interroge les planificateurs de la série Planners au lieu d'en écrire un ([ICT-Greffe2](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Greffe2-EspaceAtteignable.ipynb)). La valeur d'une information pour un petit animat y est calculée deux fois, avec Infer.NET et avec PyMC, par les outils de la théorie de la décision ([ICT-12e](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-12e-Value-of-Information-Animat-Python.ipynb)). Les extensions d'un cadre d'argumentation de Dung y sont calculées telles que la série Tweety les outille ([`ict/argumentation.py`](../../MyIA.AI.Notebooks/IIT/ICT-Series/ict/argumentation.py)), et le banc d'humour le plus exigeant de la théorie des jeux ([GameTheory-18d](../../MyIA.AI.Notebooks/GameTheory/GameTheory-18c-Humour-Banc-Python.ipynb)) y est exécuté tel quel.

Et il y a la noix. Suivie jusqu'ici comme un pur problème de mathématiques, elle est devenue le sol sur lequel ICT mesure l'émergence dans le Jeu de la Vie, en s'appuyant sur le théorème `hashlife_correct` ([ICT-Life](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Life-SubstratCertifie.ipynb)). Mais un pont ne vaut que son pilier le plus faible : ce théorème est vrai mais **vide là où HashLife saute** — son hypothèse de cadre ne peut jamais être satisfaite quand le saut s'exerce (`p5_large_n_hyps_unsat`, [`HashlifeCorrectness.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean)). C'est une autre face de la même obstruction : le cadre était trop étroit. Le théorème qui couvre vraiment les sauts existe pourtant (celui de la route neuve, déjà déposé dans la vitrine [#17465](https://github.com/jsboige/CoursIA/issues/17465)) ; le pont reste à reposer sur ce pilier-là, et ICT a raison, en attendant, de doubler la preuve d'une calibration contre les motifs canoniques. Un problème de mathématiques pures se retrouve ainsi au cœur de la recherche.

Le sens inverse existe aussi, et il est plus précieux, car c'est la recherche qui rend à l'enseignement. Le lake des jeux répétés présente son seuil de coopération, `δ ≥ (T − R) / (T − P)`, démontré en Lean, comme le test falsifiable d'[ICT-13](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-13-AxelrodStrategicMorphodynamics-Python.ipynb) sur les stratégies d'Axelrod ([README](../../MyIA.AI.Notebooks/GameTheory/game_theory_lean/README.md)). Le notebook de post-entraînement sur le piratage de récompense ([PT_07](../../MyIA.AI.Notebooks/GenAI/PostTraining/PT_07_rewardspy_reward_hacking.ipynb)) renvoie à [ICT-25](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-25-InoculationRL-Python.ipynb) comme à sa suite : ICT reprend la même récompense piratable et demande ce que le piratage fait à l'identité du modèle. L'analyse d'argumentation rejoue sur le corpus réel d'Argumentum le banc de recollement qu'[ICT-34](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-34-BancRecollementLectures-Python.ipynb) avait monté sur des objets synthétiques, et le verdict tient : sur les entrées disputées, la règle de recollement apprise bat le meilleur spécialiste ([Strate6](../../MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-Obs-04-Recollement-Strate6-Python.ipynb)). Et quand un pont n'est qu'une ressemblance, il le dit : la percolation annonce son « pont vers ICT-28 » comme une *analogie de structure, pas une identité* ([Percolation](../../MyIA.AI.Notebooks/Probas/Applications/Percolation/Percolation-Supercritique.ipynb)). Un pont qui déclare son grade, c'est un pont sur lequel on peut marcher.

Entre les séries d'enseignement elles-mêmes, de nouvelles tresses se sont nouées. Le même raisonnement — Socrate est un homme, donc mortel — est *répondu* par le raisonneur Tweety et *certifié* par le noyau de Lean, la micro-théorie étant écrite « la même » des deux côtés ([Tweety-02d](../../MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02d-FOL-Lab-Lean.ipynb), [`FolBridge.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FolBridge.lean)) ; la logique modale suit ([`ModalBridge.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/ModalBridge.lean)). En théorie des jeux, deux programmes qui lisent chacun le code de l'autre coopèrent parce qu'un théorème de logique, celui de Löb, est démontré dans le lake voisin ([`FairBot.lean`](../../MyIA.AI.Notebooks/GameTheory/game_theory_lean/ProgramGames/FairBot.lean)). Le Sudoku charge directement les bibliothèques de la série SMT. Et une seule notion, l'attribution, traverse trois séries : les valeurs de Shapley qui expliquent un modèle ([2.14b](../../MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.14b-XAI-Shap-Attribution-Causal-Bridge.ipynb)), le calcul causal qui rappelle que « choisir une baseline d'attribution, c'est choisir un estimand causal » ([CausalBridges-01-Do-Calculus](../../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)), et la valeur de Shapley des groupes en théorie des jeux coopératifs ([GameTheory-15f](../../MyIA.AI.Notebooks/GameTheory/GameTheory-15f-Shapley-Groupes-Python.ipynb)). Même le web sémantique a appris à justifier ses réponses : chaque triplet qu'il infère porte désormais une preuve rejouable ([SW-16](../../MyIA.AI.Notebooks/SymbolicAI/SemanticWeb/SW-16-Python-ProofCarryingOntologies.ipynb)).

Au-dessus des deux versants veillent les grands noms, chacun avec son Epic. Mais un nom n'entre pas dans le dépôt parce qu'on le cite : il y entre quand une série exécute ce qu'il a pensé. Serre y est entré par des diptyques où le même énoncé est calculé en Python et démontré en Lean ([Serre 100](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/README.md)), et par une carte qui rattache sa moitié du pont à la formalisation de Grothendieck ([`SerreMap.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SerreMap.lean)). Tegmark, par une boucle en trois temps : le cours d'apprentissage automatique exécute les diagrammes de phase du *grokking* ([2.9c](../../MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours/2.9c-Grokking-Diagrammes-Phases.ipynb)), un lake démontre les lois conservées qu'on en extrait ([`Grokking.lean`](../../MyIA.AI.Notebooks/ML/learning_theory_lean/EffectiveTheory/Grokking.lean)), et ICT mesure la géométrie des concepts appris ([ICT-41](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41-SAE-GeometrieFeatures-Python.ipynb)).

Schmidhuber a un organe dans ICT ([`ict/beauty.py`](../../MyIA.AI.Notebooks/IIT/ICT-Series/ict/beauty.py)) et un verdict exécuté : « le compression-progress de Schmidhuber tient » ([ICT-17b](../../MyIA.AI.Notebooks/IIT/ICT-Series/ICT-17b-Grokking-CompressionProgress-Python.ipynb)). Aaronson a fait de l'écart entre permanent et déterminant un compte d'opérations, avec l'algorithme de Ryser déjà présent dans le Sudoku ([Complexity-05b](../../MyIA.AI.Notebooks/Complexity/Complexity-05b-AaronsonArkhipov-PermanenteBosonSampling.ipynb)). Pearl a trouvé sa démonstration par la machine : deux modèles causaux qui produisent les mêmes données et prédisent des interventions opposées ([CausalBridges-01-Do-Calculus](../../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-01-Do-Calculus.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../../MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb)). D'autres attendent : Russell, cité partout, n'habite qu'un notebook, le jeu de l'interrupteur ([GameTheory-15](../../MyIA.AI.Notebooks/GameTheory/GameTheory-15-CooperativeGames-Python.ipynb)). Les Epics le mesurent elles-mêmes : plusieurs de ces noms *hantent* encore le dépôt plus qu'ils ne l'*habitent*, et c'est en les faisant habiter que naissent les ponts.

Prenons de la hauteur. Le dépôt est un site, au sens du deuxième mouvement : les séries en sont les ouverts, les ponts les recouvrements, et l'accord sur les recouvrements la condition de recollement. Là où deux séries s'accordent — Tweety et Lean sur le même syllogisme, Infer.NET et PyMC sur la même valeur d'information — une connaissance plus globale apparaît. Là où elles divergent, ou ne se ressemblent que par la structure — la percolation et l'adoption collective, la preuve de HashLife et le saut qu'elle ne couvrait pas —, l'écart n'est pas un échec : c'est une obstruction, et elle montre où travailler. C'est une image, de grade C, et elle se déclare comme telle. Mais elle dit juste : la mer ne monte plus autour d'une seule noix, elle monte entre les séries.

## Pourquoi ce geste, maintenant

L'affaire n'est pas seulement formelle. À mesure que l'IA passe aux grands modèles de langage, plusieurs séries refont d'elles-mêmes le même geste : prendre la sortie fluide mais incertaine d'un modèle, et la réécrire dans un cadre qui se vérifie. L'apprentissage symbolique reboucle un LLM sur une vérification logique ([`SL-9`](../../MyIA.AI.Notebooks/SymbolicAI/SymbolicLearning/SL-9-LLM-SymbolicLearning.ipynb)) ; l'analyse d'argumentation traduit le langage naturel en sémantiques formelles qu'on peut interroger ([`Tweety`](../../MyIA.AI.Notebooks/SymbolicAI/Tweety/), [`Argument_Analysis`](../../MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/)) ; le planificateur confronte une intention dite en mots à un solveur qui tranche ([`Planners-10`](../../MyIA.AI.Notebooks/SymbolicAI/Planners/04-NeuroSymbolic/Planners-10-LLM-Planning.ipynb)) ; le contrat écrit avec un LLM se relit à l'aune de sa vérification formelle ([`SC-11`](../../MyIA.AI.Notebooks/SymbolicAI/SmartContracts/02-Solidity-Advanced/SC-11-LLM-Assisted-Python.ipynb)). Changer de représentation vers le vérifiable cesse alors d'être une élégance : c'est le garde-fou. Lu d'un bout à l'autre, le dépôt soutient à voix basse une thèse simple : l'IA digne de confiance sera grothendieckienne par nécessité, car elle consistera à trouver le cadre où une affirmation devient contrôlable.

Cette lecture ne remplace aucun chantier. L'hommage au *langage* de Grothendieck dans Mathlib est allé à son terme ([#1646](https://github.com/jsboige/CoursIA/issues/1646)), le portage de HashLife a livré ses structures ([#1647](https://github.com/jsboige/CoursIA/issues/1647), [#2062](https://github.com/jsboige/CoursIA/issues/2062)), et la noix a suivi sa propre route ([#6724](https://github.com/jsboige/CoursIA/issues/6724), [#11161](https://github.com/jsboige/CoursIA/issues/11161)). La lecture passe au-dessus d'eux, et les relie.

## Une clé, pas une cathédrale

Ce que cette lecture demande est volontairement petit. Un document, celui-ci. Une conclusion au notebook [Lean-15-Grothendieck-Tribute](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb), qui referme l'hommage au langage de Grothendieck sur ce *geste*. Quelques liens depuis les séries citées. Pas de nouvelle série, pas d'encyclopédie : une clé n'a pas à être plus grande que la porte.

La clé a d'ailleurs déjà servi. En relisant le dépôt ainsi, une coquille a sauté aux yeux : le README de `sensitivity_lean` annonçait la direction triviale d'une inégalité, là où le code prouve le vrai théorème de Huang ([#2064](https://github.com/jsboige/CoursIA/pull/2064) l'a corrigé). Le même réflexe — demander de quoi, exactement, une hypothèse protège — a révélé qu'un garde de HashLife ne protégeait de rien, puis que le théorème sur lequel ICT fonde son substrat était vide là où il comptait. Une grille de contrôle n'aurait rien vu ; une lecture suivie, si.

Reste la noix, et regardez ce qui lui est arrivé pendant la lecture. Pierre au premier paragraphe, elle est devenue un énoncé à la première montée, un cas de recollement à la deuxième ; puis un problème dont on a démontré que le cadre était l'obstruction ; on a changé le cadre, et elle s'est ouverte ; enfin, un pilier sur lequel la recherche peut prendre appui. Personne n'a frappé. C'est exactement ce que la mer sait faire.

Ce texte a fait subir le même traitement à son propre sujet. Il ne définit nulle part ce qu'est une « lecture grothendieckienne » : il a laissé la définition monter — un changement de représentation, un recollement, une exigence de garantie, puis des ponts — jusqu'à ce qu'elle se tienne seule. Il aurait pu être un tableau, une ligne par série, une colonne par garantie. Mais un tableau découpe en fragments ce qui n'est qu'un seul geste. La bonne représentation d'un fil continu est une prose continue ; et chaque réécriture, en la rendant plus simple, fait monter l'eau d'un cran de plus. La mer, pas le burin.

---

### Annexe — Grades de certification

Cette échelle vaut partout, pas seulement en Lean. Être en grade C n'est pas un défaut ; présenter un grade C comme un grade A en est un.

| Grade | Mécanisme | Confiance | Portée |
|-------|-----------|-----------|--------|
| **A — noyau** | `rfl` / `decide` vérifiés par le noyau Lean | maximale | plafonne en taille |
| **B — compilateur de confiance** | `native_decide` (code compilé, axiome `ofReduceBool`) | élevée | passe à l'échelle |
| **C — ouvert** | test, backtest, évaluation, `#eval` | aucune garantie machine | déclarée comme telle |

Une hypothèse nommée dans un énoncé n'est pas un cran de cette échelle : c'est une dette lisible dans la signature du théorème. Un `sorry` est un trou dans une preuve. Les confondre ferait perdre ce que cette annexe sert à mesurer.

| Série | Grade dominant | Ce qui est certifié |
|-------|----------------|---------------------|
| **Sensitivity** (Lean-12) | A | Théorème de Huang complet, 0 `sorry` |
| **Notebooks pédagogiques** | A→C déclaré | Règle « une sortie = une lecture, placée immédiatement après la cellule lue » maintenant enforceable par organe ([#17040](https://github.com/jsboige/CoursIA/issues/17040), [#17471](https://github.com/jsboige/CoursIA/pull/17471) — détection de la seconde lecture sans en-tête via diff base..head) |
| **Grothendieck** (Lean-15) | A sur le langage ; C documentaire sur la lecture d'ICT | Sites, faisceaux, schémas, cohomologie (Čech, Mayer-Vietoris), 0 `sorry` ([#1646](https://github.com/jsboige/CoursIA/issues/1646)) |
| **Serre 100** | A sur les pendants Lean ; C sur les calculs Python | Borne de Hasse, orthogonalité des caractères, lemme de Yoneda sur des catégories finies |
| **Logique formelle** (Tweety ↔ Lean) | A côté Lean ; C côté raisonneur | Syllogisme du premier ordre, tables de vérité, validité de K et contre-modèles de T, 4, 5 |
| **Hecke** | A | Principalité de ℤ[ζ₇], ℤ[ζ₁₁], ℤ[ζ₁₃] |
| **Conway / HashLife** (Lean-16) | A sur les batteries (`decide` pur) ; B où `native_decide` subsiste | Correction générale du moteur décorrélé ([#17465](https://github.com/jsboige/CoursIA/issues/17465)) ; un unique `sorry` sur l'ancien cadre ([#6724](https://github.com/jsboige/CoursIA/issues/6724)) |
| **Contextualité** (Lean-13) | A | Kochen-Specker ; borne de Tsirelson atteinte par le témoin de Pauli |
| **Knots** (nœud de Conway) | C assumé | Prérequis Mathlib énumérés, horizons en décennies |
| **GameTheory** | A sur les portages Lean ; C sur les simulations | Arrow, Shapley, Bondareva-Shapley, mariages stables ; un `sorry` assumé sur le théorème *Folk* escompté |
| **SmartContracts** | C → B (fuzzing, invariants), A visé | Transitions d'état et invariants |
| **Sudoku** (Sudoku-13) | C, mesuré et croisé entre moteurs | 9×9 par appartenance régulière pure |
| **Probas, Planners, SymbolicLearning** | C | Inférences, plans, hypothèses vérifiables |
| **RL, ML, GenAI, QuantConnect** | C | Rendement, évaluation, performance hors échantillon |
| **IIT / ICT** | C | Φ sur petits systèmes ; l'obstruction au recollement comme lecture documentaire ([#4588](https://github.com/jsboige/CoursIA/issues/4588)) |

### Réconciliation avec les Epics

| Epic | Rapport à cette lecture |
|------|-------------------------|
| [#1646](https://github.com/jsboige/CoursIA/issues/1646) Hommage Grothendieck (fermée) | Le socle : #1646 montre le langage *dans* le dépôt ; ce document lit le dépôt *avec* le geste. |
| [#1647](https://github.com/jsboige/CoursIA/issues/1647) / [#2062](https://github.com/jsboige/CoursIA/issues/2062) / [#2162](https://github.com/jsboige/CoursIA/issues/2162) Conway/HashLife (fermées), [#17465](https://github.com/jsboige/CoursIA/issues/17465) vitrine | La noix : les structures, puis la vitrine qui en porte le détail. |
| [#6724](https://github.com/jsboige/CoursIA/issues/6724) · [#11161](https://github.com/jsboige/CoursIA/issues/11161) | L'ancien cadre, où l'obstruction a été démontrée, et la route neuve de Gosper, par où la noix s'est ouverte. |
| [#11162](https://github.com/jsboige/CoursIA/issues/11162) | Nouveauté contre confinement : la correction autorise la vitesse, elle ne la donne pas. |
| [#4588](https://github.com/jsboige/CoursIA/issues/4588) ICT · [#8182](https://github.com/jsboige/CoursIA/issues/8182) | Le troisième mouvement : l'obstruction comme invariant ; le socle topos de Schreiber, au grade A côté physique, C côté conscience. |
| [#12208](https://github.com/jsboige/CoursIA/issues/12208) · [#13564](https://github.com/jsboige/CoursIA/issues/13564) | Les deux règles du dialogue entre versants : mûrir avant d'infuser ; poser le problème et laisser l'outil natif calculer. |
| [#16334](https://github.com/jsboige/CoursIA/issues/16334) Serre · [#16741](https://github.com/jsboige/CoursIA/issues/16741) Tegmark · [#16775](https://github.com/jsboige/CoursIA/issues/16775) Schmidhuber · [#16781](https://github.com/jsboige/CoursIA/issues/16781) Aaronson · [#16620](https://github.com/jsboige/CoursIA/issues/16620) causalité · [#10763](https://github.com/jsboige/CoursIA/issues/10763) Tao · [#17528](https://github.com/jsboige/CoursIA/issues/17528) Russell & Norvig | Les grands noms : un auteur entre par ce qu'une série exécute, pas par une citation. |
| [#1203](https://github.com/jsboige/CoursIA/issues/1203) / [#1206](https://github.com/jsboige/CoursIA/issues/1206) / [#1210](https://github.com/jsboige/CoursIA/issues/1210) | Les trois bibliothèques externalisées. |
| [#2137](https://github.com/jsboige/CoursIA/issues/2137) Argumentum (fermée) | Pipeline LLM + Tweety : un changement de représentation vers le vérifiable. |

---

*Repères vérifiables :*

- [`conway_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/) — `Conway/Life/Hashlife.lean` (`jumpAt_capture_centered`) ; `Conway/Life/HashlifeCorrectness.lean` (`one_jumpAt_correct`, `evolveHashlifeFastAtN_correct_uncond`, `hashlife_correct`) et `HashlifeCorrectness/Foundation.lean` (`p5_large_n_hyps_unsat`) ; `Conway/Life/JumpCapture.lean` (`no_padding_depth_suffices`, `jumpCaptured_not_trivial`) ; `Conway/Life/HashlifeMarginFragment.lean` (l'unique `sorry` du lake).
- [`sensitivity_lean/Sensitivity/MainTheorem.lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/MainTheorem.lean) (`huang_degree_theorem`).
- [`game_theory_lean`](../../MyIA.AI.Notebooks/GameTheory/game_theory_lean/) — `SocialChoice/Arrow.lean`, `CooperativeGames/Shapley.lean`, `ProgramGames/FairBot.lean` ; [`GameTheory-4/4b/4c`](../../MyIA.AI.Notebooks/GameTheory/GameTheory-04-NashEquilibrium-Python.ipynb) (Nash).
- [`knot_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/) — `Knots/Conway.lean`, `Knots/MathlibPrerequisites.lean`.
- [`grothendieck_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/) et [Lean-15](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb) — [`SheafCohomology`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SheafCohomology/Basic.lean), [Mayer-Vietoris](../../MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/Grothendieck/SheafCohomology/MayerVietoris.lean), `SerreMap.lean`.
- [`hecke_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/hecke_lean/) et [`serre100_lean`](../../MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/serre100_lean/), pendants des lignes Hecke et Serre 100 de l'annexe.
- Comptes de `sorry` : `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep`.