Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions docs/grothendieckian-lens.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
12 changes: 6 additions & 6 deletions docs/index.qmd
Original file line number Diff line number Diff line change
Expand Up @@ -54,26 +54,26 @@ 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.

### [Lean](lean/coordinator-workflow.md)

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*).

## Pour les apprenants

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
Loading