Skip to content

docs(symbolic-ai,#17510): audit fichier-entier README + ajout série Geometry volée 01-02 #17815

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
Sep 26, 2026
Merged

docs(symbolic-ai,#17510): audit fichier-entier README + ajout série Geometry volée 01-02 #17815

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
80c86b2
docs(symbolic-ai,#17510): audit fichier-entier SymbolicAI/README + aj…
jsboige Sep 25, 2026
8bee872
docs(symbolic-ai,#17510): résoudre le verdict CHANGES_REQUESTED Herme…
jsboige Sep 25, 2026
c932647
Merge branch 'main' into docs/17510-symbolic-ai-geometry
jsboige Sep 25, 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
19 changes: 10 additions & 9 deletions MyIA.AI.Notebooks/SymbolicAI/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ La série SymbolicLearning (21 notebooks : 12 Python + 8 jumeaux C# from-scratch

### Parcours alternatif : Preuve automatique en géométrie (Geometry, en ouverture)

La série Geometry (programme gradué, Epic #17544) ouvre la **démonstration automatique** de théorèmes géométriques : le fil rouge (milieu de l'hypoténuse équidistant des trois sommets) est d'abord vérifié numériquement (Schwartz–Zippel), puis démontré exactement par bases de Gröbner, puis par la méthode de Wu — avant un pont vers Lean. Le notebook d'entrée [Geometry-01](Geometry/Geometry-01-From-Figure-To-Equation.ipynb) (public Découverte, ~30 min) ne suppose que la géométrie du lycée et Python de base.
La série Geometry (programme gradué, Epic #17544) ouvre la **démonstration automatique** de théorèmes géométriques : le fil rouge (milieu de l'hypoténuse équidistant des trois sommets) est d'abord vérifié numériquement (Schwartz–Zippel), puis démontré exactement par bases de Gröbner, puis par la méthode de Wu — avant un pont vers Lean. Le notebook d'entrée [Geometry-01](Geometry/Geometry-01-From-Figure-To-Equation.ipynb) (public Découverte, ~30 min) ne suppose que la géométrie du lycée et Python de base. Le second [Geometry-02](Geometry/Geometry-02-From-Equation-To-Proof.ipynb) (public Licence) ajoute l'idéal des hypothèses, la base de Gröbner et le traitement des **non-dégénérescences** (saturation) — il consomme Geometry-01 et introduit l'algèbre polynomiale en cours de route.

---

Expand Down Expand Up @@ -500,15 +500,16 @@ Documentation complète : [SymbolicLearning/README.md](SymbolicLearning/README.m

## Geometry - Preuve Automatique en Géométrie

Série en ouverture (Epic #17544, première volée 01-02-03 en cours de livraison) : la **démonstration automatique** de théorèmes de géométrie élémentaire par l'algèbre des polynômes. Un théorème fil rouge — le milieu de l'hypoténuse équidistant des trois sommets — est traversé par des méthodes de plus en plus fortes.
Série en ouverture (Epic #17544, volée 01-02 livrée, 03-05 en préparation) : la **démonstration automatique** de théorèmes de géométrie élémentaire par l'algèbre des polynômes. Un théorème fil rouge — le milieu de l'hypoténuse équidistant des trois sommets — est traversé par des méthodes de plus en plus fortes.

### Structure détaillée

| # | Notebook | Contenu | Exercices | Prérequis |
|---|----------|---------|-----------|-----------|
| 01 | [Geometry-01-From-Figure-To-Equation](Geometry/Geometry-01-From-Figure-To-Equation.ipynb) | Hypothèses/conclusion en polynômes, vérification numérique sur 10 000 figures, témoin négatif, Schwartz–Zippel et preuve probabiliste | 3 | Géométrie lycée, Python |
| 02 | [Geometry-02-From-Equation-To-Proof](Geometry/Geometry-02-From-Equation-To-Proof.ipynb) | Idéal des hypothèses, base de Gröbner (`sympy.groebner`), certificat d'appartenance de la conclusion, traitement des **non-dégénérescences** par saturation | 3 | Geometry-01, algèbre polynomiale |

> Les positions 02 (Gröbner, `sympy.groebner`), 03 (méthode de Wu, reprise de #17511), 03b (décomposition de Ritt), 04/04b (DD+AR, IMO-AG-30) et 05 (pont formel Lean) sont cadrées dans l'Epic #17544 et se livrent par volées — le chemin principal ne suppose jamais un notebook non encore publié.
> Les positions 03 (méthode de Wu, reprise de #17511), 03b (décomposition de Ritt), 04/04b (DD+AR, IMO-AG-30) et 05 (pont formel Lean) sont cadrées dans l'Epic #17544 et se livrent par volées — le chemin principal ne suppose jamais un notebook non encore publié.

Documentation complète : [Geometry/README.md](Geometry/README.md)

Expand Down Expand Up @@ -597,8 +598,9 @@ SymbolicAI/
│ ├── reference/ # Notes AIMA ch. 19
│ └── README.md
│
├── Geometry/ # Preuve automatique en géométrie (série en ouverture, Epic #17544)
├── Geometry/ # Preuve automatique en géométrie (volée 01-02, Epic #17544)
│ ├── Geometry-01-From-Figure-To-Equation.ipynb # Découverte : figure -> polynômes, Schwartz-Zippel
│ ├── Geometry-02-From-Equation-To-Proof.ipynb # Licence : Gröbner + saturation (non-dégénérescences)
│ └── README.md
│
├── SMT/ # Solveurs SMT (Satisfiability Modulo Theories) — 46 notebooks (cf. marqueur CATALOG-STATUS)
Expand Down Expand Up @@ -760,7 +762,7 @@ Le setup est entièrement automatisé via `Tweety-01-Setup-Python.ipynb` :

## Audit Qualité (septembre 2026 — §E whole-file)

### Couverture exercices (réconciliation disque ↔ marqueur ↔ prose, mise à jour 4 septembre 2026)
### Couverture exercices (réconciliation disque ↔ marqueur ↔ prose, mise à jour 25 septembre 2026)

| Série | Notebooks | Avec exercices | Sans exercices | Status |
|-------|-----------|----------------|----------------|--------|
Expand All @@ -773,11 +775,9 @@ Le setup est entièrement automatisé via `Tweety-01-Setup-Python.ipynb` :
| SymbolicLearning (AIMA ch. 19 + SL-12 differentiable logic gates) | 21 | 21 (100%) | 0 | Excellent |
| SMT/Z3-Linq2Z3 (C# Linq2Z3) | 18 | 18 (100%) | 0 | Excellent |
| SMT/Z3-API (Python + 6 jumeaux C#) | 28 | 28 (100%, 22 Python + 6 C# jumeaux) | 0 | Excellent |
| Geometry (ouverture 23/09, Epic #17544) | 1 | 1 (100%, Geometry-01 avec 3 exercices) | 0 | Série en ouverture |
| Geometry (ouverture 23/09, Epic #17544) | 2 | 2 (100%, Geometry-01/02 avec 3 exercices chacun) | 0 | Volée 01-02 livrée, 03-05 en préparation |

**Total** : le compte courant des notebooks pédagogiques **fait foi dans le bloc `<!-- CATALOG-STATUS -->` ci-dessus** (régénéré quotidiennement par `.github/workflows/catalog-cron.yml`) ; en date du 4 septembre 2026 il s'établit à **262** (y compris `root=1` : OR-tools-Stiegler, et le probe IKVM compté dans Tweety=34), hors les 4 fichiers `_archive/` (Fast-Downward-Legacy, 2 précurseurs EML SymbolicLearning, `Tweety.ipynb` legacy). Les notebooks sans exercices sont uniquement : les setups (SC-1-Setup-Foundry), les notebooks de projet (SC-26-Final-Project), la référence historique RDF.Net-Legacy, les deux dérivés Lean sans cellules d'exercice (Lean-16i, Lean-20b), l'artefact `_agent` et le groupe-I2 d'Argument Analysis, et le probe IKVM (non pédagogique).

> **Note (04/09, réconciliation fichier-entier — See #3973)** : décompositions vérifiées sur disque : **Tweety 34** = 14 Python + 18 C# + 1 Lean (Tweety-5b) + 1 probe ; **Lean 49** = 19 preuves natives (3 `lean4` + 16 `lean4-wsl`) + 30 companions Python (25 `python3` + 4 `python3-wsl` + 1 `global-3.13`) ; **SemanticWeb 27** = 13 C# (incl. RDF.Net-Legacy) + 14 Python (SW-14/15 ajoutés après la réconciliation c.1297) ; **Planners 25** = 15 Python + 9 C# jumeaux + 1 Lean (Planners-5b) ; **SmartContracts 31** = 30 Python + 1 `lean4-wsl` (SC-7c) ; **Argument_Analysis 28** = 10 Agentic (7 sources + 3 artefacts `_agent.ipynb`) + 17 analytiques + 1 groupe-I2 ; **SymbolicLearning 21** = 12 Python + 8 C# jumeaux + 1 Lean (SL-1b) ; **SMT 46** = 28 Z3-API (22 Python + 6 C# jumeaux) + 18 Z3-Linq2Z3 ; root = 1. Réconciliation précédente : 15 août 2026 (c.118, total 230). Ajout 23 septembre 2026 : **Geometry 1** = Geometry-01-From-Figure-To-Equation (série en ouverture, Epic #17544 ; le catalogue la comptera à sa prochaine régénération). Pour les comptes courants, le marqueur `<!-- CATALOG-STATUS -->` fait foi.
**Total** : le compte courant des notebooks pédagogiques **fait foi dans le bloc `<!-- CATALOG-STATUS -->` ci-dessus** (régénéré quotidiennement par `.github/workflows/catalog-cron.yml`) ; le catalogue est la source de vérité — il se resynchronise au prochain cron, et la table §E ci-dessus est un instantané daté. Les notebooks sans exercices sont uniquement : les setups (SC-1-Setup-Foundry), les notebooks de projet (SC-26-Final-Project), la référence historique RDF.Net-Legacy, les deux dérivés Lean sans cellules d'exercice (Lean-16i, Lean-20b), l'artefact `_agent` et le groupe-I2 d'Argument Analysis, et le probe IKVM (non pédagogique).

### Problèmes connus (juillet 2026)

Expand Down Expand Up @@ -879,6 +879,7 @@ La famille SymbolicAI est couverte sur **trois stacks** selon les formalismes (E
| **Argument Analysis** | ● (24 sources, hors 3 artefacts `_agent` et 1 groupe-I2) | — | — | Pipeline SK multi-agents + port verbatim EPITA-IS Argumentum (couches Python) |
| **SymbolicLearning** | ● (12) | ◐ (8 jumeaux) | ◐ (1, SL-1b) | AIMA ch. 19 induction pure + ILP + neuro-symbolique ; jumeaux from-scratch BCL-only dont SL-6c FOIL |
| **SMT / Z3** (Z3-Linq2Z3 + Z3-API) | ● (22) | ● (24) | — | Z3-Python API complète + 6 jumeaux C# (#4956) + Z3.Linq DSL C# 18 nb (missionnaires, cryptarithms, sudoku) |
| **Geometry** (Epic #17544) | ● (2) | — | — | Preuve automatique en géométrie : figure → polynômes (Schwartz–Zippel), équation → preuve (Gröbner + saturation) |

Légende : ● couverture large ; ◐ couverture partielle / companion ; — absent.

Expand Down
Loading