diff --git a/docs/grothendieckian-lens.md b/docs/grothendieckian-lens.md index c3d5d5d686..9b64233870 100644 --- a/docs/grothendieckian-lens.md +++ b/docs/grothendieckian-lens.md @@ -90,11 +90,11 @@ Et il y a la noix. Suivie jusqu'ici comme un pur problème de mathématiques, el 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.ipynb) sur les stratégies d'Axelrod ([README](../MyIA.AI.Notebooks/GameTheory/repeated_games_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.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.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/Argument_Analysis_Recollement_Strate6.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 » ([Do-Calculus-Bridge](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/Do-Calculus-Bridge.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.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)). +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.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.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.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-05](../MyIA.AI.Notebooks/Complexity/Complexity-05-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 ([Do-Calculus-Bridge](../MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/Do-Calculus-Bridge.ipynb)). Tao a digéré et formalisé une preuve récente de la conjecture de Sendov ([Lean-18](../MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.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.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. +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.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-05](../MyIA.AI.Notebooks/Complexity/Complexity-05-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/Lean-18-Sendov-Complex-Analysis.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.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. diff --git a/docs/index.qmd b/docs/index.qmd index a33f9222bb..1d761d2ca0 100644 --- a/docs/index.qmd +++ b/docs/index.qmd @@ -54,11 +54,11 @@ Réparation env Python (règle F : installer le kernel/env, jamais contourner). Setup environnement, validation notebooks, slash commands. -### [Curriculum](../curriculum/ia-classique.md) et [Curriculum GenAI](../curriculum/genai.md) +### [Curriculum](curriculum/ia-classique.md) et [Curriculum GenAI](curriculum/genai.md) Plans d'apprentissage par école (ECE, ESGF, EPITA, EPF), scope pédagogique. -### [Grothendieckian lens](../grothendieckian-lens.md) +### [Grothendieckian lens](grothendieckian-lens.md) Perspective unificatrice sur les séries du dépôt, à la Grothendieck. @@ -66,7 +66,7 @@ Perspective unificatrice sur les séries du dépôt, à la Grothendieck. Prover iteration history, intractable diagnosis, LLM endpoints. -### [QC](../qc/quantconnect.md) +### [QC](qc/quantconnect.md) Backtests, MCP Docker, structure, livre référence (*Hands-On AI Trading*). @@ -74,6 +74,6 @@ Backtests, MCP Docker, structure, livre référence (*Hands-On AI Trading*). Si vous venez d'arriver et cherchez à **apprendre** (pas à contribuer) : -1. [PARCOURS](../../parcours.qmd) — trois parcours certifiés selon votre niveau -2. [README.md](../../README.md) — vue d'ensemble du dépôt -3. [Catalogue](../../COURSE_CATALOG.generated.md) — inventaire exhaustif et à jour +1. [PARCOURS](../parcours.qmd) — trois parcours certifiés selon votre niveau +2. [README.md](../README.md) — vue d'ensemble du dépôt +3. [Catalogue](../COURSE_CATALOG.generated.md) — inventaire exhaustif et à jour