Skip to content

fix(prose,#5081): README SymbolicAI -- clause Serre100 au futur alors que #17789 est merge #20667

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 3 commits into from
Oct 16, 2026
Merged

fix(prose,#5081): README SymbolicAI -- clause Serre100 au futur alors que #17789 est merge #20667

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7e6a6e6
fix(prose,#5081): README SymbolicAI -- clause Serre100 au futur alors…
jsboige Oct 14, 2026
27060fd
Merge branch 'main' into fix/17789-serre100-stale-prose
myia-po-2023 Oct 14, 2026
279816d
Merge origin/main into fix/17789-serre100-stale-prose (content-free b…
jsboige Oct 16, 2026
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
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/SymbolicAI/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ Chaque série se présente en trois temps : ce qu'elle apprend, son **parcours l
- **Parcours léger** — 1 à 6, les fondations : installation, types dépendants, propositions et preuves (Curry-Howard), quantificateurs, mode tactique, Mathlib4. Puis 7 à 10, la preuve à l'ère des LLMs : intégration LLM, preuve agentique, orchestration multi-agents, LeanDojo.
- **Chapitres thématiques** — à partir de 11, chaque numéro ouvre un chapitre qui suppose les fondations et se choisit selon son intérêt : réseaux de neurones vérifiés (11), théorème de sensibilité de Huang (12), contextualité de Kochen-Specker (13), hommages à Grothendieck (15) et à Conway (16), théorie des nœuds (17), puis les digestions de résultats récents (Sendov, *Analysis I* de Tao, PFR, détection MIMO, problème inverse de Galois pour M₂₃…).
- **Pour approfondir** — les lettres sont surtout des **compagnons** : un compagnon Lean natif (`-Native`, kernel Lean) qui prouve ce que le notebook principal raconte, ou un compagnon Python qui l'illustre. Les preuves vivent dans des **lakes** (`sensitivity_lean`, `conway_lean`, `knot_lean`, `grothendieck_lean`, `galois_lean`…).
- **Sous-série** — [Serre100](Lean/Serre100/README.md) a sa propre numérotation et son lake `serre100_lean`. Un notebook d'escalier dans le parcours principal la présentera et y renverra (#17789). Ce modèle doit ensuite servir aux familles de chapitres les plus denses, comme Conway et Grothendieck.
- **Sous-série** — [Serre100](Lean/Serre100/README.md) a sa propre numérotation et son lake `serre100_lean`. Le notebook d'escalier du parcours principal la présente et y renvoie ([Lean-37-Capstone-Serre100](Lean/Lean-37-Capstone-Serre100.ipynb), #17789). Ce modèle doit ensuite servir aux familles de chapitres les plus denses, comme Conway et Grothendieck.
- [README de la série Lean](Lean/README.md)

### SMT / Z3 — décider sous contraintes
Expand Down
Loading