[EPIC] Knot Theory Lean — scaffolding, invariants, Conway knot & Piccirillo proof #2874

État mesuré au 2026-10-05 — relevé de la lane myia-ai-01:CoursIA-2 sur main.
Ce bloc est un relevé, pas une réécriture : l'historique des phases ci-dessous est conservé tel quel.
Portée : l'état du lake à cette date. Les cases déjà cochées n'ont pas été re-vérifiées.

Ce que ce body dit, et ce qui est mesuré

Confrontation case par case (les 13 cases non cochées)

Évolution depuis la rédaction de ce body

verifyMoves_sound (Knots/ReidemeisterCombinatorial.lean:235), le seul site de sorry à route bornée du lake, est prouvé (#19107, mergée le 2026-10-04) : le compte de sorry réels passe de 9 à 8. La phase qui le porte n'apparaît pas dans ce body, le fait est donc consigné ici pour que le relevé soit complet.

Livraisons mergées non inscrites (relevé scripts/epic_body_staleness.py)

Cinq PRs mergées citent cet EPIC sans que le corps les inscrive. Relues une par une :

Sortie retenue

Le body est corrigé, l'EPIC n'est pas replié. Restent réellement ouverts : les tangles, la notation de Conway, la construction par mutation (partielle), l'invariance (à reformuler), et les trois entrées permanentes ou partielles de la Phase 5.

Non vérifié

• Les cases déjà cochées (Phases 1 et 1b, début de la Phase 2) n'ont pas été re-vérifiées.
• La répartition des 8 sorry par déclaration n'a pas été re-mesurée ici : elle vit dans knot_lean/README.md §sorries, dont la table attribue encore 4 sorry à Knots/Conway.lean alors que la mesure les situe dans Knots/Slice.lean (extraction lean(knot,#2874): refondre Conway.lean en sous-fichiers progressifs avec commentaires de digestion #18397) — la table du README est en retard d'un cran sur ce point.

État au 2026-09-01 — la mesure du 30/08 tient, les citations de ligne avaient dérivé

Passe de curation (défaut #13906). Cet EPIC fait exception : ses en-têtes datés sont
exacts, et la mesure du jour les confirme au chiffre près —
python scripts/lean/count_code_sorry.py --json rend 11 déclarations distinctes
sur 22 tokens pour knot_lean, sur un total dépôt de 15 distinctes / 30 tokens,
soit les 73,33 % annoncés le 30/08. Rien à réfuter.

Deux choses ont malgré tout été corrigées ci-dessous, et ce sont celles qu'une lane
heurte en pratique :

1. Quatre citations de ligne avaient dérivé — le fichier a grossi depuis le 23/08.
   tricolorable_invariant 3489 → 3515 · Knot.unknottingNumber 2221 → 2247 ·
   tricolorable_invariant_r2_connected 3322 → 3214 ·
   tricolorable_invariant_r3_connected 3474 → 3500. Elles étaient justes à leur
   date ; une ligne citée ne se vérifie que le jour où on la lit.
2. Les cases du corps historique étaient toutes vides, y compris pour du travail
   livré. Un en-tête qui dit « corps conservé pour l'historique » ne se voit pas quand
   on scrolle jusqu'à une liste de cases : cinq sont cochées avec leur artefact nommé,
   et les deux qui restent ouvertes disent désormais pourquoi.

Ce qui reste vraiment ouvert, en clair : le nombre de croisements du nœud de huit
(aucun théorème n'existe — seul figureEight_not_tricolorable est là) et le dernier
sorry d'Invariant.lean (Knot.unknottingNumber, Phase 4+).

Correction du 2026-09-02 — la phrase précédente sur la Phase 3-4 était fausse deux fois

La version du 01/09 disait : « le front de Phase 3-4 reste définitionnel
(IsSmoothlySlice, IsTopologicallySlice, conway_trivial_alexander,
KT_trivial_alexander) : ce sont des def … := sorry — définir n'attend aucune
infrastructure Mathlib absente. » Relecture des sites : les deux moitiés sont fausses,
et une lane qui aurait suivi cette phrase aurait perdu son cycle. Le front se sépare en
deux régimes que rien ne devrait confondre :

Site	Forme réelle	Ce qu'il attend
IsSmoothlySlice (Conway.lean:509), IsTopologicallySlice (:517)	def … := sorry	de l'infrastructure Mathlib absente, et le site le documente lui-même : 4-ball (not in Mathlib), properly embedded surfaces (not in Mathlib), plongements lisses D²→B⁴ absents. Définir fidèlement n'est pas à portée. C'est la moitié que la phrase du 01/09 niait
conway_trivial_alexander (:486), KT_trivial_alexander (:496)	theorem … := by exact sorry	rien d'absent. Ce sont des théorèmes, pas des définitions. Cible vérifiée hors Lean (census PD spherogram 2.4.1, sonde validée sur 3_1/4_1/5_1) : mineur = −t⁶ et t⁵, deux unités. Route de preuve écrite au site : déterminant du noyau de la matrice creuse 10×10 sur ℤ[t]. Matrix.det et Polynomial sont dans Mathlib

Autrement dit, le grain tractable de cette EPIC n'est pas celui que la phrase désignait :
ce sont les deux polynômes d'Alexander, bornés, à cible connue et à route nommée. Les
deux def slice sont, eux, la seule vraie dette d'infrastructure du lake — à laisser
telle quelle et à ne pas rouvrir sans Mathlib.

La leçon de méthode est la même que celle que ce corps porte déjà : quatre sorry cités
ensemble ne forment pas une classe. Ouvrir les quatre sites aurait pris deux minutes ;
ne pas les ouvrir a produit une phrase qui inversait la portée sur la moitié d'entre eux.

État vérifié des réfutations Vibe — 2026-08-30

L'audit Vibe du 2026-08-29 a comparé des mesures courantes à des strates
historiques datées, puis a qualifié trois écarts de REFUTE. La chronologie Git
et les mesures canoniques montrent au contraire que les trois affirmations étaient
exactes à leur date et ont ensuite été dépassées par des livraisons. Les sections
historiques restent conservées ci-dessous comme snapshots datés.

Réfutation Vibe	Chronologie vérifiée	Verdict
MyIA.AI.Notebooks/GameTheory/knot_lean/	Le scaffolding a été créé sous ce chemin le 2026-06-12 (09f15936e6, puis #2875). La relocation vers MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/ a été mergée le lendemain, le 2026-06-13, par #2893 (8164bc6d47).	RÉFUTATION REJETÉE — chemin historique exact à l'ouverture, devenu obsolète après relocation.
26 tokens sorry sur 13 déclarations distinctes	Snapshot canonique avant #12406 : code_sorry=26, distinct_code_sorry=13. #12406 a ensuite retiré AreMutants (13 → 12, merge 2026-08-23, 8dabb36f98), puis #12892 a retiré alexanderPolynomial (12 → 11, merge 2026-08-28, 883c6e9f5b). Mesure courante : 22 tokens sur 11 déclarations distinctes.	RÉFUTATION REJETÉE / SUPERSEDÉ — la mesure actuelle confirme deux décharges ultérieures ; elle ne réfute pas le snapshot daté.
13 des 17 sorry du dépôt — 76 %	Au même snapshot, 13 / 17 = 76,47 %, honnêtement arrondi à 76 %. #12406 documente le passage dépôt 17 → 16 et lake 13 → 12 ; après #12892, l'état courant est 11 / 15 = 73,33 % (équivalent tokens FR/EN : 22 / 30).	RÉFUTATION REJETÉE / SUPERSEDÉ — proportion historique arithmétiquement exacte, devenue 73,33 % après deux preuves livrées.

Instrument canonique : python scripts/lean/count_code_sorry.py --json, champ
distinct_code_sorry pour la dette dédupliquée FR/EN. code_sorry compte les deux
siblings et ne doit pas être confondu avec le nombre de déclarations distinctes.

État mesuré au 2026-08-23 — lire ceci avant le corps historique

Delta du 2026-08-23 — la révision du 20/08 ci-dessous était elle-même périmée
sur son point central : elle désignait tricolorable_invariant comme « le front de
Phase 2 », alors qu'il est prouvé depuis. Corrigé dans le tableau des destins.
Le sous-grain AreMutants est provisionné (greenlight ai-01 du 23/08, lane
myia-po-2024:CoursIA) : définition combinatoire au niveau PD, deux siblings FR/EN,
acceptance distinct_code_sorry 13 → 12 + lake build SUCCESS + deux lemmes de
discrimination (positif conwayKnot/kinoshitaTerasakaKnot, négatif trefoil/unknot)
— sans quoi une définition trop lâche rendrait le −1 cosmétique.

Le corps ci-dessous date du 12/06/2026 et n'a jamais été rafraîchi. Trois de
ses affirmations les plus consultées sont fausses aujourd'hui, et ce sont
précisément elles qui rendent cette Epic impiochable — c'est le mécanisme par
lequel elle est restée délaissée 68 jours, pas un manque d'intérêt du sujet :

Le corps dit	Réalité mesurée le 20/08
« PR #2875 en review », « PR #2878 en review », « Aucune des deux n'est mergée — attente review ai-01 »	Les deux sont mergées le 13/06/2026. Un lecteur qui suit cette phrase part réviser une PR vieille de deux mois, ou conclut que le coordinateur bloque l'Epic
MyIA.AI.Notebooks/GameTheory/knot_lean/	Le lake vit sous MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/. Un ls sur le chemin du corps rend vide — un zéro qui ressemble à « rien n'existe »
Phase 2 : « sorry → 0 sur Knots/Invariant.lean »	Invariant.lean porte 2 sorry, dont un seul relève de la Phase 2 (l'autre est Phase 4+)

Ce qui a réellement été livré depuis

• Phase 1 + 1b mergées (feat(knot-theory): scaffolding knot_lean + Lean-17a notebook (See #2874) #2875, feat(Lean-17b): Knot Invariants Companion notebook (Phase 1b, See #2874) #2878, 13/06). Trois notebooks vivent : Lean-17-Knots-a-Conway-and-Proofs, Lean-17-Knots-b-Invariants-Companion, et Lean-17c-Knots-Companion-Formel (feat(knot,#11703): companion formel knot_lean - Lean-17c (Basic/Invariant/Reidemeister par leurs declarations) #11882, mergé le 20/08 — companion formel adressant Basic/Invariant/Reidemeister par leurs déclarations).
• i18n FR/EN complète : 6 paires siblings (docs(lean,#4980): knot_lean/Knots root aggregator FR-first bilingual inline #6156, i18n(#4980): knot_lean/Knots/Basic FR-first sibling pair (foundations) #6421, i18n(#4980): knot_lean/Knots/Reidemeister FR-first sibling pair (R-moves equivalence) #6429, i18n(#4980): knot_lean/Knots/MathlibPrerequisites FR-first sibling pair (Phase 0 INDEX) #6437, i18n(#4980): add knot_lean/Knots/Invariant_en sibling (EN mirror) #6581, i18n(lean,#4980): knot_lean/Knots root FR-first sibling pair #6682, i18n(#4980): knot_lean/Knots/Reidemeister canonical FR-first flip (over-claim #6429) #7686), convention i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980.
• Migration Lean v4.32.0 (feat(lean,#10986): migrate knot_lean to v4.32.0 (Phase 3, tranche 6) #11020) · CI câblée lean-knot.yml + job advisory target-coverage (ci(knot,#8782): wire advisory target-coverage job to lean-knot.yml #8794) · lean-knot SUCCESS sur main le 2026-08-19T12:29Z.
• Phase 2 très avancée, contrairement à ce que le corps laisse croire.

Dette formelle réelle — mesurée par l'outil canonique, pas par grep

python scripts/lean/count_code_sorry.py --json → 26 tokens sorry sur 13 déclarations distinctes (paires FR/EN dédoublonnées) (naive_sorry vaut 58 : la prose du lake documente abondamment ses propres sorry, d'où un facteur 4,5 si on grepe).

knot_lean porte à lui seul 13 des 17 sorry réels du dépôt entier — 76 % de toute la dette formelle. C'est la concentration la plus dense du repo, et c'est ce qui fait de cette Epic un vivier profond plutôt qu'un reliquat.

Répartition par destin, et c'est la ligne qui compte :

Destin	Décl.	Où
Phase 5 — permanents assumés (Piccirillo, Freedman, Lidman/Heegaard-Floer, théorème de Reidemeister)	5	conway_not_smoothly_slice, conway_topologically_slice, unknotting_11n102{,_upper}, reidemeister_theorem
Phase 3-4 — Conway / polynômes	6	AreMutants, alexanderPolynomial, conway_trivial_alexander, KT_trivial_alexander, IsSmoothlySlice, IsTopologicallySlice
Phase 4+ — infrastructure	1	Knot.unknottingNumber
Phase 2 — la cible actuelle CLOSE le 2026-08-23	0	tricolorable_invariant est PROUVÉ (Knots/Invariant.lean:3515, induction sur ReidemeisterEquiv, consommé par trefoil_not_unknot) — livré par #11893/#11903

Autrement dit : le front de Phase 2 est CLOS. Ce qui reste est un front de
Phase 3-4, et il est définitionnel : AreMutants, alexanderPolynomial,
IsSmoothlySlice, IsTopologicallySlice sont des def … := sorry — des
définitions stubbées, pas des preuves manquantes. C'est une nuance décisive
pour piocher ici : définir n'attend aucune infrastructure Mathlib absente,
contrairement à prouver.

tricolorable_invariant — clos le 2026-08-23 (section conservée pour l'historique)

Les trois jambes de transfert sont désormais construites, et le théorème maître les compose :

Jambe	forward	backward	statut
Reidemeister1Connected	✅ Invariant.lean:1826	✅ :2536/:2746	complète
Reidemeister2Connected	✅ :2035	✅ :3183	complète → tricolorable_invariant_r2_connected (:3214)
Reidemeister3Connected	✅ Reidemeister.lean:694	✅ :773 (#11552)	complète → tricolorable_invariant_r3_connected (Invariant.lean:3500)

Le transfert R3 qui manquait à la révision du 20/08 a été construit, et l'iff maître
tricolorable_invariant (Invariant.lean:3515) l'obtient par induction sur
ReidemeisterEquiv, chaque pas portant sa direction dans une disjonction.
trefoil_not_unknot le consomme. Il ne reste qu'un seul sorry dans tout
Invariant.lean : Knot.unknottingNumber (:2247), Phase 4+, bloqué sur une
infrastructure documentée au site (well-formedness de changeCrossing).

Sous-grain découpé et déposé : #11893.

Le corps historique est conservé intégralement ci-dessous : il porte les références bibliographiques, l'inventaire d'outillage et le plan de phases, qui restent valides. Seule sa description d'état est périmée.

Summary

Scaffolding Lean 4 pour la théorie des nœuds, avec invariants de difficulté croissante, sorry stratégiques commentés (références Mathlib), notebook pédagogique Python (visualisations + preuve Piccirillo/Lidman), et notebook compagnon Python pour le calcul effectif des invariants via SageMath/SnapPy/pyknotid.

Pattern identique aux projets existants (social_choice_lean/, conway_cgt_lean/, cooperative_games_lean/, conway_lean/, Grothendieck 13/13b) : dépendance externe + scaffolding + sorry=0 progressif.

Motivation

• Le nœud de Conway (11n34) relie John Conway à la topologie algébrique — boucle la série Lean-14 (Conway)
• La preuve de Piccirillo (doctorante, résout en 1 semaine un problème de 50 ans) est un récit pédagogique exceptionnel
• Lidman (2606.12431) montre une preuve courte mais profonde — contraste instructif
• La théorie des nœuds est un domaine visuel et intuitif, parfait pour le Lean pédagogique
• Connecte Grothendieck (topos, homologie) ↔ Conway (nœuds, jeux) ↔ formalisation
• Les invariants calculables (Alexander, Jones, HOMFLY-PT, Kauffman, Khovanov) ont des implémentations Python matures — pas besoin de Mathematica

Ressources externes identifiées

Formalisation Lean

Bases de données et calcul (Python — pas de Mathematica nécessaire)

Conclusion outillage : SageMath + SnapPy + pyknotid couvrent tout ce que Mathematica + KnotTheoryfont, en open source,pip install`. Pas besoin de licence Mathematica.

Références papier

• Piccirillo (2018/2020) : The Conway knot is not slice, Annals of Mathematics 191(2). arXiv:1808.02923
• Lidman (2026) : The unknotting number of 11n102 is 2. arXiv:2606.12431
• Reidemeister (1927) : Elementare Begründung der Knotentheorie
• Fox (1962) : A quick trip through knot theory — 3-colorabilité
• Conway (1970) : An enumeration of knots and links — notation Conway, nœud de Conway 11n34
• Prathamesh (2015) : Formalising Knot Theory in Isabelle/HOL, LNCS 9250. doi:10.1007/978-3-319-22102-1_29
• Kauffman (1987) : State models and the Jones polynomial — bracket de Kauffman
• Jones (1985) : A polynomial invariant for knots via von Neumann algebras

Phases

Phase 1 — Scaffolding + notebook pédagogique (PR #2875, MERGÉE le 2026-06-13)

Code créé et mergé (#2875, 2026-06-13).

• Créer MyIA.AI.Notebooks/GameTheory/knot_lean/ avec lakefile.lean
• Knots/Basic.lean : définitions (Knot, Link), PD-code, nœuds nommés
• Knots/Reidemeister.lean : 3 mouvements de Reidemeister (sorry avec référence)
• Knots/Invariant.lean : 3-colorabilité, nombre de croisements, nombre de dénouage
• Knots/Conway.lean : nœud de Conway (11n34), Kinoshita-Terasaka (11n42), mutation
• Knots/Lidman.lean : 11n102, unknotting number = 2 (sorry avec référence Heegaard-Floer)
• Knots/MathlibPrerequisites.lean : index des prérequis Mathlib manquants
• Notebook Lean-17-Knots-a-Conway-and-Proofs.ipynb : visualisations Python + contexte (renommé depuis Lean-14d-…, mini-arc dédié slot 17)
• README.md avec références et état scaffolding (39 sorry, ~15 permanents)

Phase 1b — Notebook compagnon Python : calcul des invariants (PR #2878, MERGÉE le 2026-06-13)

Notebook Python dédié (Lean-17-Knots-b-Invariants-Companion.ipynb) qui reproduit et vérifie tous les invariants listés sur Knot Atlas pour nos nœuds d'intérêt, en utilisant uniquement des outils Python open source. Code créé, pas encore mergé (#2878 OPEN).

Contenu prévu :

• Représentations : conversion PD-code, DT-code, Gauss code, Conway notation (livré par enrich(lean,#2874): knot representations PD/DT/Gauss/Conway (Lean-17a, C.4) #10375, mergée le 2026-08-11) (depuis katlas.org/wiki/Conway_Notation)
• K11n102 (Lidman) — tabulation complète depuis katlas.org/wiki/K11n102 :
  • Alexander polynomial : $-t^2 + t + 1 + t^{-1} - t^{-2}$ (référence Knot Atlas)
  • Conway polynomial : $-z^4 - 3z^2 + 1$ (référence Knot Atlas)
  • Jones polynomial : vérifié contre Knot Atlas
  • HOMFLY-PT polynomial (référence Knot Atlas)
  • Kauffman polynomial (référence Knot Atlas)
  • Determinant = 3, Signature = -2
  • Rasmussen s-invariant = 2
  • Hyperbolic volume = 7.24432 (SnapPy — MATCH calculé)
  • Khovanov homology grid (référence Knot Atlas)
  • Vassiliev invariants V2 = -3, V3 = 6
• K11n34 (Conway) vs K11n42 (Kinoshita-Terasaka) — comparaison systématique :
  • Même Alexander polynomial (= 1, comme l'unknot !)
  • Même volume hyperbolique (11.21912 — mutants)
  • Sliceness topologique vs lisse — illustration de la dichotomie (Piccirillo 2018)
• Nœuds classiques : unknot, trèfle (3_1), figure-eight (4_1) — validation des outils (volume SnapPy)
• Visualisations : heatmaps polynôme d'Alexander, tableaux comparatifs invariants
• Exercices étudiants (≥3, convention [Epic transverse] Convention 3 exercices par notebook #2161) : volume torus knot, classification mutants, dichotomie sliceness

Outils (pip install, pas de Mathematica) :

Phase 2 — Prouver les invariants élémentaires

• 3-colorabilité du trèfle (preuve accessible) (trefoil_tricolorable, Knots/Invariant.lean:1274, prouvé)
• Invariance de la 3-colorabilité par Reidemeister moves (tricolorable_invariant, Knots/Invariant.lean:3515, induction sur ReidemeisterEquiv)
• Nombre de croisements du trèfle = 3 (trefoil_crossing_number, Knots/Invariant.lean:2195)
• Nombre de croisements du nœud de huit = 4 — ouvert : aucun théorème de croisements sur figureEight ; seul figureEight_not_tricolorable (:2176) existe
• sorry → 0 sur Knots/Invariant.lean — 1 restant, Knot.unknottingNumber (:2247), Phase 4+, bloqué sur une infrastructure documentée au site

Phase 3 — Tangles et Conway notation

• Définition des tangles (suivre shua/leanknot Tangle.lean)
• Notation de Conway pour les nœuds
• Construction du nœud de Conway et Kinoshita-Terasaka par mutation
• Même polynôme d'Alexander par mutation

Phase 4 — Polynômes de nœuds (Jones, Alexander)

• Polynôme de Jones via bracket de Kauffman
• Polynôme d'Alexander (version Conway)
• Invariance par Reidemeister
• Distinction trèfle vs unknot via Jones

Phase 5 — Perspectives de formalisation avancée (sorry permanents)

• conway_not_smoothly_slice : prérequis = invariant s de Rasmussen, Khovanov homology, trace companion — très loin de Mathlib
• unknotting_11n102 : prérequis = Montesinos trick, Heegaard Floer d-invariants, Ni-Wu formula — très loin de Mathlib
• Documentation des prérequis Mathlib manquants comme guide pour la communauté Lean

Critères de complétion

Phase 1 (PR #2875, mergée)

• lake build SUCCESS sur knot_lean/ (CI lean-knot.yml sur main : success le 2026-09-01T14:55Z, 657ce776)
• Scaffolding compilable avec sorry commentés (39 sorry, ~15 permanents)
• Notebook Lean-17-Knots-a exécutable (Python visualisations)
• README.md avec références

Phase 1b (PR #2878, mergée)

• Notebook compagnon exécutable avec 0 erreur (9/9 cells PASS, Papermill)
• Invariants K11n102 vérifiés contre Knot Atlas (volume SnapPy 7.24432 MATCH)
• Comparaison K11n34 vs K11n42 tabulée (mutants, dichotomie sliceness)
• Visualisations polynôme d'Alexander + volume hyperbolique
• requirements.txt avec dépendances (snappy, numpy, matplotlib)

Connexions CoursIA

• Série Lean-17 (Knots Theory) : mini-arc dédié (17a: Conway & Proofs, 17b: Invariants Companion) — slot 17 free, décision user
• Série Lean-13 (Grothendieck) : pont théorique (topologie, homologie, faisceaux → invariants de nœuds)
• conway_cgt_lean/ : déjà importe vihdzp/combinatorial-games — même pattern
• social_choice_lean/ : modèle de scaffolding avec sorry résolus progressivement
• Epic [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159 (Grothendieck sheafHom) : potentielle connexion cohomologie ↔ invariants
• Epic Epic — Conway tribute Phase 2 : Game of Life, hashlife, Gemini replicator, OTCA Metapixel, CPU patterns en Lean (low priority) #1647 (Conway Phase 2) : même univers Conway

Voir aussi

• Epic — Conway tribute Phase 2 : Game of Life, hashlife, Gemini replicator, OTCA Metapixel, CPU patterns en Lean (low priority) #1647 Conway Phase 2 (hashlife + Gemini + OTCA + CPU)
• Epic — Hommage à Grothendieck : Mathlib tour, micro-formalisations, notebook Lean-13 (low priority) #1646 Grothendieck Phase 1
• [Epic Grothendieck] Avancer la formalisation Lean (au-dela de la Phase 1) #2159 Grothendieck sheafHom
• Lean AI Formalization Leaderboard
• Knot Atlas — base de données de référence
• SageMath Knot Theory
• SnapPy
• pyknotid

Epic ouverte par po-2025, mandat user 2026-06-12. Phase 1 = PR #2875, Phase 1b = PR #2878 (compagnon Python invariants) — les deux mergées le 2026-06-13.