Skip to content

Fix(docs,#22291): H1 Search-09d/09e + KNOTS-01..04 alignes sur l'ordinal du fichier (tranche 3) #22365

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 2 commits into from
Oct 25, 2026
+15 −15
Merged

Fix(docs,#22291): H1 Search-09d/09e + KNOTS-01..04 alignes sur l'ordinal du fichier (tranche 3) #22365

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ea1e46a
Fix(docs,#22291): H1 des carnets Search-09d/09e et KNOTS-01..04 align…
jsboige Oct 24, 2026
3b04f62
Fix(notebook-lean,#22291): le renvoi FigureEight.lean pointe la ligne 16
jsboige Oct 24, 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
6 changes: 3 additions & 3 deletions MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-BeckFiala-Lean-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,13 @@
"tags": []
},
"source": [
"# Discrepancy-01 - Beck-Fiala (la noix `disc <= 2k-1`) et le pont vers le lake `discrepancy_lean`\n",
"# Search-09d - Beck-Fiala (la noix `disc <= 2k-1`) et le pont vers le lake `discrepancy_lean`\n",
"\n",
"> **Premier carnet de la sous-série `Discrepancy/`.** Il expose en Python les énoncés du lake `discrepancy_lean` (Mathlib4 pinné `db584cd6`, toolchain `leanprover/lean4:v4.33.0` dans `discrepancy_lean/lean-toolchain`) et rend palpable la frontière entre ce qui est **certifié** sur `main` et ce qui ne l'est pas : une conjecture n'est jamais présentée comme un résultat. Ce notebook n'est pas une preuve formelle : il implémente un **squelette** de l'algorithme de Beck-Fiala (rounding itératif, départ `0`, phases sur les lignes dangereuses), expose les définitions Lean verbatim comme citations, et compare la discrépance obtenue à la borne `2k - 1` du théorème `beck_fiala_classic`.\n",
"\n",
"> **Précondition du théorème.** La borne `2*k - 1` de `beck_fiala_classic` n'engage que sous la précondition `maxDegree(F) ≤ k`, où `k` borne le **degré** maximal d'un sommet, et non la cardinalité des parties. Sur les instances aléatoires de la cellule 4 (`n=10, m=15, k_max=2`), cette précondition est violée pour les 40 instances (degré maximal mesuré entre 4 et 9) : la borne n'est donc pas applicable, et les cellules 3 et 5 en tirent les conséquences.\n",
"\n",
"**Navigation** : [Search README](..) ; [LEAN_INVENTORY](../LEAN_INVENTORY.md) ; [FORMAL_STATUS](../discrepancy_lean/FORMAL_STATUS.md) ; module source [BeckFiala.lean](../discrepancy_lean/Discrepancy/BeckFiala.lean). Issue de suivi : #17816.\n"
"**Navigation** : [Search README](..) ; [LEAN_INVENTORY](../LEAN_INVENTORY.md) ; [FORMAL_STATUS](../discrepancy_lean/FORMAL_STATUS.md) ; module source [BeckFiala.lean](../discrepancy_lean/Discrepancy/BeckFiala.lean). Issue de suivi : #17816."
]
},
{
Expand Down Expand Up @@ -961,4 +961,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"tags": []
},
"source": [
"# Discrepancy-02 — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n",
"# Search-09e — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n",
"\n",
"> **Deuxième marche de la sous-série `Discrepancy/`** (issue #17816, arbitrage Search #17802) — compagnon formel de [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb)\n",
"\n",
Expand Down Expand Up @@ -4480,4 +4480,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
6 changes: 3 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"tags": []
},
"source": [
"# Lean 17a — Conway, les Nœuds et la Preuve de Piccirillo\n",
"# KNOTS-01 — Conway, les Nœuds et la Preuve de Piccirillo\n",
"\n",
"**Série** : SymbolicAI / Lean — Knots Theory (**17a**)\n",
"\n",
Expand All @@ -37,7 +37,7 @@
"La section **6** recense, elle, ce qui manque encore à Mathlib — et la section\n",
"**5** décrit l'arborescence du projet.\n",
"\n",
"**Notebook compagnon** : `KNOTS-02-Invariants-Python.ipynb` — calcul effectif des invariants via SnapPy/SageMath.\n"
"**Notebook compagnon** : `KNOTS-02-Invariants-Python.ipynb` — calcul effectif des invariants via SnapPy/SageMath."
]
},
{
Expand Down Expand Up @@ -179,7 +179,7 @@
"carré parfait (condition **nécessaire** de Fox–Milnor :\n",
"$|\\Delta(-1)| = 1, 4, 9, 16, \\ldots$).\n",
"Or $\\det(4_1) = |\\Delta(-1)| = 5$ — la condition de Fox–Milnor échoue\n",
"(valeur documentée par `KNOTS/knot_lean/Knots/FigureEight.lean` ligne 17 :\n",
"(valeur documentée par `knot_lean/Knots/FigureEight.lean` ligne 16 :\n",
"`det(4_1) = |Δ(-1)| = 5`).\n",
"Attention : le déterminant non-carré n'est qu'**une** obstruction parmi\n",
"d'autres, pas un critère autonome de non-sliceness. Une seconde voie, plus\n",
Expand Down
6 changes: 3 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"tags": []
},
"source": [
"# Lean 17b — Invariants de Nœuds : Calcul et Vérification\n",
"# KNOTS-02 — Invariants de Nœuds : Calcul et Vérification\n",
"\n",
"**Série** : SymbolicAI / Lean — Knots Theory (17b = compagnon de 17a)\n",
"\n",
Expand All @@ -33,7 +33,7 @@
"- Python 3.10+ avec `snappy`, `matplotlib`, `numpy`\n",
"- `pip install snappy matplotlib numpy`\n",
"\n",
"## Durée estimée : 45 min\n"
"## Durée estimée : 45 min"
]
},
{
Expand Down Expand Up @@ -2319,4 +2319,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"tags": []
},
"source": [
"# Lean 17c — Le lake `knot_lean` par ses déclarations (compagnon formel)\n",
"# KNOTS-03 — Le lake `knot_lean` par ses déclarations (compagnon formel)\n",
"\n",
"Compagnon du **Lean-17** (« Conway, les Nœuds et la Preuve de Piccirillo »). Là où Lean-17 raconte l'histoire mathématique (Fox 3-colorabilité, mutants, Piccirillo 2020, Lidman 2026) et interroge `Conway.lean` et `Lidman.lean`, ce notebook interroge les modules que Lean-17 ne cite pas — **`Basic.lean`** (les structures fondamentales), **`Invariant.lean`** (la chaîne 3-colorabilité), **`Reidemeister.lean`** (les moves R1/R2/R3 et leurs murs) et **`MathlibPrerequisites.lean`** (la feuille de route des prérequis Mathlib) — et mesure l'état de la formalisation : déclarations par module, sorries réels vs prose, axiomes admis.\n",
"\n",
Expand Down
6 changes: 3 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
"tags": []
},
"source": [
"# Lean 17d — Géométrie hyperbolique : tétraèdres idéaux, chirurgie de Dehn, rigidité de Mostow\n",
"# KNOTS-04 — Géométrie hyperbolique : tétraèdres idéaux, chirurgie de Dehn, rigidité de Mostow\n",
"\n",
"**Série** : SymbolicAI / Lean — Knots Theory (17d = compagnon de 17a/17b/17c)\n",
"\n",
Expand All @@ -39,7 +39,7 @@
"## Prerequis\n",
"\n",
"- `pip install snappy>=3.2 mpmath>=1.3`\n",
"- lecture recommandée de KNOTS-02 (volume hyperbolique) avant ce carnet-ci : la vérification croisée présuppose de voir où le volume sort.\n"
"- lecture recommandée de KNOTS-02 (volume hyperbolique) avant ce carnet-ci : la vérification croisée présuppose de voir où le volume sort."
]
},
{
Expand Down Expand Up @@ -1088,4 +1088,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading