Lean 17c — Le lake knot_lean par ses déclarations (compagnon formel)
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.
Kernel Python par choix : le kernel natif lean4-wsl est gelé en attendant la mise à jour du binaire repl (#11874 — construit pour v4.30.0, lakes en v4.33.0). La lecture des sources reste réelle : chaque cellule ouvre le fichier .lean du lake et en extrait les déclarations, jamais une copie.
Voir knot_lean/README.md pour l’état détaillé du corridor Reidemeister.
1. Le lac : deux langues
Le lake suit la convention i18n #4980 : chaque module français a son sibling _en byte-identique sur le code, docstrings traduites. On inventorie les modules FR et leurs miroirs.
import refrom pathlib import PathLAKE = Path('knot_lean')modules =sorted(p for p in (LAKE /'Knots').glob('*.lean') ifnot p.stem.endswith('_en'))print(f"Modules FR du lake : {len(modules)}")for p in modules: en = p.with_name(p.stem +'_en.lean') sib ='oui'if en.exists() else'ABSENT'print(f" {p.name:28}{len(p.read_text(encoding='utf-8').splitlines()):>5} lignes sibling _en : {sib}")
Chaque module FR a son miroir _en — la convention i18n est respectée sur ce lake (miroirs §9). Invariant.lean est le plus gros en lignes (la chaîne 3-colorabilité, §3), Conway.lean porte le plus de déclarations, et MathlibPrerequisites est le plus concis — la feuille de route pure de §7.
2. Basic.lean — les structures fondamentales
Tout le lake repose sur quatre structures : Crossing, PDCrossing, KnotDiagram, Knot (+ Link). Les nœuds canoniques (unknot, trefoil, figureEight) y sont définis, ainsi que le miroir et le nombre de croisements.
# Declarations publiques de Basic.lean, extraites du fichier reelDECL_RE = re.compile(r'^(structure|theorem|lemma|def|instance|abbrev)\s+([A-Za-z_][A-Za-z0-9_.\'\?]*)')def decls_of(path): out = []for i, line inenumerate(path.read_text(encoding='utf-8').splitlines(), 1): m = DECL_RE.match(line)if m: out.append((i, m.group(1), m.group(2)))return outbasic = decls_of(LAKE /'Knots'/'Basic.lean')print(f"Basic.lean : {len(basic)} declarations")for ln, kind, name in basic:print(f" L{ln:>4}{kind:9}{name}")
Basic.lean : 34 declarations
L 53 structure Crossing
L 81 structure PDCrossing
L 90 structure KnotDiagram
L 109 structure Knot
L 119 structure Link
L 127 def Knot.toLink
L 137 def unknotDiagram
L 141 def unknot
L 149 def trefoilDiagram
L 157 def trefoil
L 175 def figureEightDiagram
L 184 def figureEight
L 192 def mirrorCrossing
L 198 def Knot.mirror
L 210 def Knot.crossingNumberOfDiagram
L 236 def Knot.crossingNumber
L 245 def KnotDiagram.edges
L 249 def KnotDiagram.numCrossings
L 286 def KnotDiagram.wf
L 295 theorem unknot_wf
L 299 theorem trefoil_wf
L 303 theorem figureEight_wf
L 327 theorem mirror_unknot_wf
L 334 theorem mirror_trefoil_wf
L 340 theorem mirror_figureEight_wf
L 376 theorem mirrorCrossing_perm
L 397 theorem mirrorCrossing_preserves_count
L 408 theorem count_lift_append
L 433 theorem mirror_diag_preserves_count
L 467 def mirror_diag_edges
L 481 theorem mirror_edges_subperm
L 511 theorem mirror_wf_preserves_partial
L 542 theorem mirror_edges_perm
L 560 theorem mirror_wf_preserves
Lecture du résultat
Les trois nœuds canoniques du lake sont des def explicites (unknotDiagram, trefoilDiagram, figureEightDiagram puis leurs objets Knot). wf (well-formed) est un Bool : la correction du PD-code est décidable et testée — unknot_wf en est la preuve minimale.
3. Invariant.lean — la chaîne 3-colorabilité
C’est le cœur pédagogique du lake : la définition IsTricolorable et le théorème-cible tricolorable_invariant (« la 3-colorabilité de Fox est invariante par moves de Reidemeister »), avec sa décomposition en bras ascendants R1/R2 et ses murs nommés.
# Les declarations cibles de la chaine tricolorabiliteinv = decls_of(LAKE /'Knots'/'Invariant.lean')print(f"Invariant.lean : {len(inv)} declarations\n")CIBLES = ['IsTricolorable', 'triColorFoxCondition_iff_sum_mod_three','tricolorable_invariant', 'tricolorable_forward_r1','tricolorable_forward_r2_up', 'r2_append_only_wall', 'r3_determined_wall']for ln, kind, name in inv:ifany(name.startswith(c) or c in name for c in CIBLES):print(f" L{ln:>4}{kind:9}{name}")
Invariant.lean : 86 declarations
L 234 def IsTricolorable
L 304 instance IsTricolorable.decidable
L 338 theorem triColorFoxCondition_iff_sum_mod_three
L 715 theorem tricolorable_forward_r1
L 960 theorem tricolorable_forward_r2_up
L1088 theorem r2_append_only_wall
L1241 theorem r3_determined_wall
L1380 theorem tricolorable_invariant_fails_under_pr1_model
L3356 theorem tricolorable_invariant_r2_connected
L3642 theorem tricolorable_invariant_r3_connected
L3657 theorem tricolorable_invariant
Lecture du résultat
La chaîne expose la discipline de preuve du lake : tricolorable_invariant (le théorème-cible) est décomposé en bras tricolorable_forward_r1 et tricolorable_forward_r2_up, chacun borné par des murs nommés (r2_append_only_wall, r3_determined_wall) — des theorem qui énoncent l’obligation restante au lieu de la cacher dans un sorry anonyme. La bi-implication R1 est complète (forward + backward, #11227).
4. Sorries réels vs prose — l’instrument juste
Le README du lake documente deux comptes : grep -c sorry naïf (compte la prose) et le mode real du CI (strippe commentaires, compte mot-bounded). Un grep naïf sur Invariant.lean rend un total beaucoup plus élevé que le réel. On mesure les deux.
# Les deux comptes, mesures sur les fichiers reelsdef count_sorry(path, mode): text = path.read_text(encoding='utf-8')if mode =='naive':return text.count('sorry')# mode real : strippe -- et /- -/, compte le mot bounded stripped = re.sub(r'/-([^-]|-[^/])*-/', ' ', text, flags=re.S) stripped = re.sub(r'--.*', ' ', stripped)returnlen(re.findall(r'\bsorry\b', stripped))rows = []for p in modules: rows.append([p.stem, count_sorry(p, 'naive'), count_sorry(p, 'real')])rows.append(['TOTAL', sum(r[1] for r in rows), sum(r[2] for r in rows)])import pandas as pddf = pd.DataFrame(rows, columns=['module', 'grep naif', 'sorry reels'])df
module
grep naif
sorry reels
0
Basic
3
0
1
Conway
3
0
2
FigureEight
0
0
3
Invariant
6
0
4
Jones
1
0
5
Lidman
4
2
6
MathlibPrerequisites
2
0
7
Reidemeister
2
2
8
ReidemeisterCombinatorial
4
1
9
ReidemeisterInvariance
0
0
10
ReidemeisterMoves
1
0
11
Slice
8
4
12
TOTAL
34
9
Lecture du résultat
L’écart naive/réel illustre le piège documenté dans les règles du dépôt : les docstrings FR documentent précisément l’absence de preuve (« mur R2 », « restent 2 sorries ») — un grep naïf compte cette documentation. Le CI gate sur le compte réel. Un instrument qui surestime la dette fausse l’arbitrage de ce qu’il faut prouver ensuite.
5. Reidemeister.lean — les moves et le corridor sémantique
Les moves R1/R2/R3 y sont des Prop explicites (Reidemeister1, Reidemeister2, …) avec symétries prouvées. Le corridor #8696 (5 PRs mergées) y a remplacé le move-surgery with par des égalités de champs. Des sorries réels subsistent : reidemeister_theorem (topologie PL des 3-variétés, hors Mathlib actuel — documenté INTRINSIC).
# Les moves Reidemeister et leurs proprietesreid = decls_of(LAKE /'Knots'/'Reidemeister.lean')print(f"Reidemeister.lean : {len(reid)} declarations\n")for ln, kind, name in reid: tag =''if name.startswith('Reidemeister'): tag =' <-- move'print(f" L{ln:>4}{kind:9}{name}{tag}")
Reidemeister.lean : 36 declarations
L 87 def Reidemeister1 <-- move
L 97 theorem Reidemeister1.symm <-- move
L 145 def Reidemeister1' <-- move
L 164 theorem Reidemeister1'.implies_reidemeister1 <-- move
L 217 def PDCrossing.isRenameOf
L 229 def PDCrossing.hasEdge
L 262 def Reidemeister1Connected <-- move
L 286 theorem reidemeister1Connected_satisfiable
L 320 theorem Reidemeister1Connected.numEdges_succ <-- move
L 328 theorem Reidemeister1Connected.numCrossings_succ <-- move
L 337 theorem Reidemeister1Connected.shares_edge <-- move
L 350 theorem Reidemeister1Connected.crossings_eq <-- move
L 374 def Reidemeister2 <-- move
L 383 theorem Reidemeister2.symm <-- move
L 414 def PDCrossing.isDoubleRenameOf
L 444 def Reidemeister2Connected <-- move
L 466 theorem reidemeister2Connected_satisfiable
L 494 theorem Reidemeister2Connected.numEdges_succ <-- move
L 502 theorem Reidemeister2Connected.numCrossings_succ <-- move
L 521 def Reidemeister3 <-- move
L 532 theorem Reidemeister3.symm <-- move
L 580 def PDCrossing.isSlotPermOf
L 590 def Reidemeister3Determined <-- move
L 606 theorem Reidemeister3Determined.implies_reidemeister3 <-- move
L 622 theorem reidemeister3Determined_satisfiable
L 694 def Reidemeister3Connected <-- move
L 716 theorem reidemeister3Connected_satisfiable
L 736 theorem Reidemeister3Connected.numCrossings_eq <-- move
L 743 theorem Reidemeister3Connected.numEdges_eq <-- move
L 773 def Reidemeister3ConnectedInv <-- move
L 791 theorem reidemeister3ConnectedInv_satisfiable
L 817 theorem reidemeister3Connected_inv
L1013 theorem reidemeister_equiv_symm
L1025 theorem reidemeister_equiv_equivalence
L1036 def KnotEquiv
L1053 theorem reidemeister_theorem
Lecture du résultat
Chaque move a sa .symm prouvée (la symétrie n’est pas une hypothèse cachée). Reidemeister1Connected vient avec ses théorèmes de comptage (numEdges_succ, numCrossings_succ) : le modèle R1-connecté rend le move localement vérifiable — c’est ce qui a permis le corridor.
6. Trois modules nés après la première rédaction
Ce compagnon a été écrit quand le lake tenait en six modules. Le lake a grandi, et trois modules du corridor des moves n’ont jamais été montrés ici : ReidemeisterMoves, ReidemeisterCombinatorial et FigureEight.
Ce n’est pas un détail cosmétique. L’audit de visibilité de l’EPIC #11703 compte les modules dont aucune déclaration n’apparaît dans un notebook : un travail formel qu’aucun lecteur ne peut lire. Ces trois modules figuraient parmi les modules invisibles du lake. Cette section ferme l’écart en extrayant leurs déclarations, comme les sections 2 à 5 le font pour les modules d’origine.
6.1 ReidemeisterMoves.lean — la relation de moves comme type inductif
Reidemeister.lean (§5) décrit les moves un par un. ReidemeisterMoves.lean prend un pas de plus : il pose la relation de moves comme un type inductif, dont source et target sont des fonctions, et sur lequel se définit la notion d’affinement de codes PD.
# ReidemeisterMoves.lean : declarations et signatures des objets structurants# Jeu de mots-cles large : le DECL_RE de la section 2 omettait `inductive`,# or les deux types structurants de cette section en sont (ReidemeisterMove,# MoveSequence). Aligne sur l'organe de visibilite (EPIC #11703), qui inclut# inductive/class/opaque dans son propre extracteur.DECL_WIDE = re.compile(r'^(theorem|lemma|def|abbrev|instance|structure|inductive|class|opaque)\s+([A-Za-z_][A-Za-z0-9_.\'\?]*)')def decls_wide(path): out = []for i, line inenumerate(path.read_text(encoding='utf-8').splitlines(), 1): m = DECL_WIDE.match(line)if m: out.append((i, m.group(1), m.group(2)))return outdef statement_of(path, name, max_lines=7):"""Lignes du fichier a partir de la declaration `name`, jusqu'au `:=`. Extrait du fichier reel -- jamais reecrit a la main.""" lines = path.read_text(encoding='utf-8').splitlines()for i, line inenumerate(lines): m = DECL_WIDE.match(line)if m and m.group(2) == name: out = [line]for nxt in lines[i +1:i + max_lines]:ifnot nxt.strip():break out.append(nxt)if':='in nxt or nxt.rstrip().endswith('where'):breakreturn"\n".join(out)returnf"(introuvable : {name})"rm = LAKE /'Knots'/'ReidemeisterMoves.lean'moves = decls_wide(rm)print(f"ReidemeisterMoves.lean : {len(moves)} declarations")for ln, kind, name in moves:print(f" L{ln:>4}{kind:9}{name}")print()for target in ('SameRelOn', 'RefinesOn', 'ReidemeisterMove'):print(statement_of(rm, target))print(' ---')
ReidemeisterMoves.lean : 31 declarations
L 74 def SameRelOn
L 82 def RefinesOn
L 88 lemma SameRel.sameRelOn
L 94 instance decidableSameClass
L 102 lemma forall_le_iff_all_range
L 126 inductive ReidemeisterMove
L 138 def ReidemeisterMove.source
L 144 def ReidemeisterMove.target
L 171 def crossingAt
L 176 instance decidableIsRenameOf
L 182 instance decidableIsDoubleRenameOf
L 188 instance decidableHasEdge
L 199 def verifyR1Fwd
L 218 def verifyR2Fwd
L 242 def verifyR3Fwd
L 267 def verifyR1
L 270 def verifyR2
L 275 def verifyR3
L 279 def verifyMove
L 295 def verifyMoves
L 303 def movesConnects
L 326 theorem verifyR1Fwd_sound
L 377 theorem verifyR2Fwd_sound
L 433 theorem verifyR3Fwd_sound
L 477 theorem verifyMove_sound
L 501 theorem verifyMoves_sound
L 521 theorem movesConnects_sound
L 541 theorem reidemeister1Connected_arcPartition_sameRelOn_witness
L 562 theorem reidemeister2Connected_arcPartition_refinesOn_witness
L 584 theorem reidemeister3Connected_arcPartition_sameRelOn_witness
L 596 theorem reidemeister3Connected_witness_movesConnects
def SameRelOn (n : Nat) (P Q : List (List Nat)) : Prop :=
∀ ⦃x y : Nat⦄, x ≤ n → y ≤ n → (SameClass P x y ↔ SameClass Q x y)
---
def RefinesOn (n : Nat) (fine coarse : List (List Nat)) : Prop :=
∀ ⦃x y : Nat⦄, x ≤ n → y ≤ n → (SameClass fine x y → SameClass coarse x y)
---
inductive ReidemeisterMove : Type where
/-- Création/suppression d'une boucle (kink). -/
| r1 (source target : KnotDiagram) : ReidemeisterMove
/-- Ajout/retrait d'une paire de croisements (bigon). -/
| r2 (source target : KnotDiagram) : ReidemeisterMove
/-- Glissement triangulaire. -/
| r3 (source target : KnotDiagram) : ReidemeisterMove
---
Lecture du résultat
ReidemeisterMoves ne décrit plus des moves isolés mais la relation elle-même : ReidemeisterMove est un type inductif, source/target en sont les projections, et RefinesOn compare deux familles de mouvements sur un même code PD. C’est le cadre dont verifyMoves a besoin pour parler de « suite de moves » sans énumérer les cas à la main.
6.2 ReidemeisterCombinatorial.lean — le vérificateur décidable
Ce module contient la pièce la plus intéressante du corridor : un vérificateur exécutable. verifyMoves est une fonction Bool qui décide si deux diagrammes sont reliés par une suite de moves de longueur bornée, et verifyMoves_sound prouve que ce oui/non machine ne ment jamais. C’est le motif « décider par le calcul, garantir par la preuve » — un booléen rapide à exécuter, adossé à un théorème qui dit exactement ce qu’il affirme.
# ReidemeisterCombinatorial.lean : le verificateur decidable et sa garantierc = LAKE /'Knots'/'ReidemeisterCombinatorial.lean'combi = decls_wide(rc)print(f"ReidemeisterCombinatorial.lean : {len(combi)} declarations")for ln, kind, name in combi:print(f" L{ln:>4}{kind:9}{name}")print()for target in ('MoveSequence', 'verifyMoves', 'verifyMoves_sound'):print(statement_of(rc, target))print(' ---')
ReidemeisterCombinatorial.lean : 10 declarations
L 79 inductive MoveSequence
L 107 def movesConnects
L 122 theorem movesConnects_sound
L 143 def ReidemeisterStep.toWitness
L 166 def oneStepWitnesses
L 188 def verifyMovesAux
L 199 def verifyMoves
L 222 theorem verifyMoves_sound
L 246 def foldChangeCrossingsAt
L 251 structure UnknottingWitness
inductive MoveSequence : KnotDiagram → KnotDiagram → Type where
/-- Suite vide : un diagramme se relie trivialement à lui-même. -/
| nil (d : KnotDiagram) : MoveSequence d d
/-- Enchaîner un pas `ReidemeisterStep d₁ d₂` avec une suite `MoveSequence d₂ d₃`. -/
| cons {d₁ d₂ d₃ : KnotDiagram}
(step : ReidemeisterStep d₁ d₂)
(tail : MoveSequence d₂ d₃) :
---
def verifyMoves (n : Nat) (d₁ d₂ : KnotDiagram) : Bool :=
verifyMovesAux n d₁ d₂
---
theorem verifyMoves_sound :
∀ (n : Nat) (d₁ d₂ : KnotDiagram),
verifyMoves n d₁ d₂ = true → ReidemeisterEquiv d₁ d₂ := by
---
Lecture du résultat
La paire verifyMoves / verifyMoves_sound est le cœur exécutable du lake : le booléen décide, le théorème garantit. Un lecteur qui veut auditer la recherche combinatoire peut exécuter le vérificateur ; un lecteur qui veut la certitude lit la garantie. Les deux vivent dans le même module, ce qui interdit de les faire diverger.
6.3 FigureEight.lean — le nœud en huit, Alexander et 3-colorabilité
Le nœud en huit est le premier nœud amphichiral : il est identique à son miroir. FigureEight.lean le formalise — diagramme planaire, signes de croisement, polynôme d’Alexander, et deux faits contrastés : le nœud en huit n’est pas 3-coloriable, là où le trèfle l’est. La formalisation couvre aussi l’invariance sous miroir, qui est précisément ce qui distingue le huit du trèfle.
# FigureEight.lean : le noeud en huit et ses invariantsfe = LAKE /'Knots'/'FigureEight.lean'fig8 = decls_wide(fe)print(f"FigureEight.lean : {len(fig8)} declarations")for ln, kind, name in fig8:print(f" L{ln:>4}{kind:9}{name}")print()for target in ('alexander_figureEightPlanar_classical','alexander_figureEightPlanar_signed_mirror','figureEightPlanarDiagram_not_tricolorable'):print(statement_of(fe, target))print(' ---')
FigureEight.lean : 12 declarations
L 78 theorem crossingSigns_figureEightPlanarDiagram
L 91 theorem alexander_figureEightPlanar_signed
L 105 theorem alexander_figureEightPlanar_classical
L 120 theorem alexander_figureEightPlanar_signed_mirror
L 136 theorem alexander_figureEightPlanar_eval_neg_one
L 151 theorem alexander_figureEightPlanar_unsigned
L 166 theorem alexander_figureEightPlanar_unsigned_eval_neg_one
L 185 theorem figureEightPlanarDiagram_not_tricolorable
L 193 theorem figureEightPlanarDiagram_numCrossings
L 198 def figureEightPlanar
L 203 theorem figureEightPlanar_wf
L 218 theorem figureEightPlanar_crossingNumber_provisional
theorem alexander_figureEightPlanar_classical :
∃ (k : ℕ) (ε : ℤ), ε * ε = 1 ∧
alexanderPolynomialSigned figureEightPlanarDiagram [false, false, true, true]
= Polynomial.C ε * Polynomial.X ^ k * (Polynomial.X ^ 2 - 3 * Polynomial.X + 1) := by
---
theorem alexander_figureEightPlanar_signed_mirror :
alexanderPolynomialSigned figureEightPlanarDiagram [true, true, false, false]
= -(Polynomial.X ^ 2 - 3 * Polynomial.X + 1) := by
---
theorem figureEightPlanarDiagram_not_tricolorable :
¬ IsTricolorable figureEightPlanarDiagram := by
---
Lecture du résultat
Le contraste est le sujet : le trèfle est 3-coloriable, le huit ne l’est pas ; et le huit est amphichiral, ce que la formalisation du miroir capture. Ces théorèmes ne sont pas décoratifs — ce sont les premiers invariants classiques du lake, calculés sur un diagramme planaire explicite.
7. MathlibPrerequisites.lean — la feuille de route des prérequis
Ce module ne prouve rien — et c’est son rôle. Chacune de ses déclarations est un théorème volontairement vide (True := trivial) : ce qui compte n’est pas l’énoncé mais la docstring au-dessus, qui documente ce que Mathlib ne sait pas encore faire pour tel résultat de théorie des nœuds (Epic #2874, Phase 1). Trois tiers de difficulté annoncent trois horizons : Tier 1 accessible (les cibles Phase 2), Tier 2 modéré (Alexander, Jones), Tier 3 approfondi (le théorème de Reidemeister, Piccirillo, Lidman, Freedman — les mêmes résultats que Lean-17 raconte historiquement).
# Les 11 prerequis, extraits du fichier reel, avec tier / enjeu / referencemp_path = LAKE /'Knots'/'MathlibPrerequisites.lean'mp_text = mp_path.read_text(encoding='utf-8')print(f"MathlibPrerequisites.lean : {len(decls_of(mp_path))} declarations, {count_sorry(mp_path, 'real')} sorry reel\n")rows = []tier, enjeu, ref =None, None, ''for line in mp_text.splitlines(): m = re.match(r'.*-!\s*## (Tier \d)\s*:\s*(\S+)', line)if m: tier =f"{m.group(1)} ({m.group(2)})"continue m = re.match(r'/--\s*(#\d+\s*:.*)', line)if m: enjeu = m.group(1)continue m = re.match(r'Reference\s*:\s*(.*)', line)if m: ref = m.group(1)continue dm = DECL_RE.match(line)if dm: rows.append([tier, dm.group(2), enjeu, ref]) enjeu, ref =None, ''for t, name, enjeu, ref in rows:print(f" {t:22}{name:42}{enjeu}")if ref:print(f" {'':22}{'':42} ref. {ref}")print()df_mp = pd.DataFrame(rows, columns=['tier', 'declaration', 'enjeu', 'reference'])df_mp.groupby('tier', sort=False).size().rename('declarations').to_frame()
MathlibPrerequisites.lean : 11 declarations, 0 sorry reel
Tier 1 (Accessible) pd_wellformed_prerequisites #1 : Bien-fondation des PD-codes
Tier 1 (Accessible) trefoil_tricolorable_prerequisites #2 : Le trefoil est tricoloriable
Tier 1 (Accessible) unknot_not_tricolorable_prerequisites #3 : Le noeud trivial n'est pas tricoloriable
Tier 1 (Accessible) tricolorable_invariant_prerequisites #4 : La tricolorabilite est invariante sous R1, R2, R3
Tier 2 (Modere) reidemeister_formal_prerequisites #5 : Mouvements de Reidemeister (description formelle)
ref. shua/leanknot possede une formalisation partielle.
Tier 2 (Modere) alexander_polynomial_prerequisites #6 : Polynome d'Alexander
ref. Alexander (1928), Crowell & Fox (1963)
Tier 2 (Modere) jones_polynomial_prerequisites #7 : Polynome de Jones via le crochet de Kauffman
ref. Jones (1985), Kauffman (1987)
Tier 3 (Approfondi) reidemeister_theorem_prerequisites #8 : Isotopie ambiante <-> equivalence de Reidemeister
ref. Reidemeister (1927), Alexander (1928)
Tier 3 (Approfondi) piccirillo_prerequisites #9 : Theoreme de Piccirillo (Conway non lisse-slice)
ref. Piccirillo (2018), arXiv:1808.02923
Tier 3 (Approfondi) lidman_prerequisites #10 : Theoreme de Lidman (nombre de denouement de 11n102 = 2)
ref. Lidman (2026), arXiv:2606.12431
Tier 3 (Approfondi) freedman_prerequisites #11 : Theoreme de Freedman (Conway topologiquement slice)
ref. Freedman (1982), J. Differential Geom.
declarations
tier
Tier 1 (Accessible)
4
Tier 2 (Modere)
3
Tier 3 (Approfondi)
4
Lecture du résultat
Les déclarations, sans sorry réel, sont classées « vacuous markers » par l’instrument du dépôt (count_code_sorry.py) — ce ne sont pas de la dette de preuve, ce sont de la documentation formalisée.
Le Tier 1 cible exactement la chaîne 3-colorabilité de §3 (bien-fondé des PD-codes, tricoloriable du trèfle, non-tricoloriable du nœud trivial, invariance R1/R2/R3) — la feuille de route a vieilli dans le bon sens : ce sont ces cibles que §3-§4 montrent en cours de réalisation (bras, murs nommés, sorry restants localisés). Le Tier 2 prolonge le corridor de §5 : description formelle des moves, polynôme d’Alexander via Burau/Fox, polynôme de Jones via le crochet de Kauffman. Le Tier 3 est l’horizon de recherche : le théorème de Reidemeister (isotopie ambiante ↔︎ moves) et le trio du nœud de Conway — Piccirillo (non lisse-slice), Freedman (topologiquement slice), Lidman (dénouement de 11n102) — les deux premiers inscrits au Lean AI Leaderboard. Chronologie annoncée pour ce tier : « années à décennies ».
La feuille de route et l’histoire racontée par Lean-17 se répondent : ce que Lean-17 présente comme résultats mathématiques établis (Piccirillo 2020, Lidman 2026), ce module l’écrit comme ce que Mathlib devrait construire pour qu’ils deviennent des théorèmes Lean.
8. Le tableau de bord du lake
Synthèse : déclarations, sorries réels, et théorèmes-phare par module.
# Tableau de bord : declarations / theoremes / sorries reels par modulerows = []for p in modules: ds = decls_of(p) thm =sum(1for _, k, _ in ds if k in ('theorem', 'lemma')) rows.append([p.stem, len(ds), thm, count_sorry(p, 'real')])df = pd.DataFrame(rows, columns=['module', 'declarations', 'theoremes', 'sorries reels'])df['sorries/decl'] = (df['sorries reels'] / df['declarations']).round(2)df
module
declarations
theoremes
sorries reels
sorries/decl
0
Basic
34
14
0
0.00
1
Conway
98
77
0
0.00
2
FigureEight
12
11
0
0.00
3
Invariant
86
59
0
0.00
4
Jones
72
35
0
0.00
5
Lidman
7
5
2
0.29
6
MathlibPrerequisites
11
11
0
0.00
7
Reidemeister
36
22
2
0.06
8
ReidemeisterCombinatorial
9
2
1
0.11
9
ReidemeisterInvariance
19
18
0
0.00
10
ReidemeisterMoves
30
12
0
0.00
11
Slice
5
3
4
0.80
Lecture du résultat
MathlibPrerequisites porte le cadre sans sorry réel ; Basic est propre ; Conway et Invariant sont déchargés (split #14821) — la dette se concentre dans Slice (le ratio le plus lourd du tableau) et le pair Lidman/Reidemeister, plus le squelette d’organe ReidemeisterCombinatorial (#18615). Le ratio sorries/declarations rend lisible où porte l’effort de preuve restant.
9. Le miroir i18n — byte-identity du code
La convention #4980 exige que seules les docstrings et commentaires diffèrent entre Foo.lean et Foo_en.lean. Vérification mesurée : on retire prose et commentaires des deux fichiers et on compare.
# Byte-identity via l'instrument canonique du depot# (check_i18n_siblings.py : la byte-identity est MODULO les lignes qui# differentent legitimement -- import/open/namespace _en, suffixes _en --# un check naive du code brut rendrait des faux NON. On localise le repo# en remontant depuis le cwd jusqu'au dossier scripts/.)import subprocess, sysfrom pathlib import Pathroot = Path.cwd()whilenot (root /"scripts"/"lean"/"check_i18n_siblings.py").exists(): root = root.parentr = subprocess.run( [sys.executable, str(root /"scripts"/"lean"/"check_i18n_siblings.py"), "knot_lean"], capture_output=True, text=True, cwd=str(root /"MyIA.AI.Notebooks"/"SymbolicAI"/"Lean"),)out = (r.stdout or r.stderr).strip().splitlines()print(out[-1] if out elsef"(aucune sortie, rc={r.returncode})")
Le lake est en état i18n drained : toutes les paires sont byte-identiques au sens canonique (modulo import/open/namespace _en et les suffixes _en d’identifiants — les seules lignes qui diffèrent légitimement), seules les docstrings diffèrent réellement. C’est la garantie que le sibling EN ne dérive jamais du FR. Un test naïf du code brut rendrait des faux négatifs — c’est exactement pourquoi le dépôt a un instrument canonique.
Exercice 1 — Les murs nommés
Les murs (r2_append_only_wall, r3_determined_wall) sont la signature de la discipline de preuve du lake : énoncer l’obligation restante au lieu de la cacher. Retrouvez leur ligne exacte dans Invariant.lean et le texte de l’énoncé.
Indice : cherchez les theorem dont le nom contient wall. Attention, l’énoncé peut être sur plusieurs lignes — capturez aussi la ligne suivante.
Étape 1 : lister toutes les déclarations dont le nom contient wall. Étape 2 : pour chaque mur, afficher ses 2 premières lignes d’énoncé.
# Exercice a completer : localiser les murs nommes d'Invariant.lean# Etape 1 : noms des declarations contenant 'wall'# Etape 2 : pour chacune, les 2 premieres lignes suivant la declarationpass
Exercice 2 — Le compte qui fonde la baseline CI
Le CI gate sur 9 sorries réels (lean-knot.yml sorry-baseline: "9", post-#18615). Recomptez avec l’instrument real ci-dessus et confrontez à la baseline.
Indice : la fonction count_sorry(path, 'real') est déjà écrite. Le résultat doit être comparé à la constante 9 — un écart dans un sens ou l’autre est un signal (régression ou baseline périmée).
Étape 1 : total real sur les modules. Étape 2 : afficher la comparaison au format total vs baseline : OK/ECART.
# Exercice a completer : confrontez le compte real a la baseline CI (9)BASELINE =9pass
Exercice 3 — Votre premier mur
La discipline du lake : quand une preuve résiste, on ne met pas un sorry anonyme — on énonce le mur. Écrivez (en Python, pour l’analyse) un détecteur de sorries anonymes : un sorry dont le théorème enveloppant ne porte ni wall ni commentaire d’explication.
Indice : parcourez les lignes ; quand vous croisez sorry en mode réel, remontez au theorem/def englobant et vérifiez si son nom ou les 5 lignes au-dessus contiennent wall ou --.
Étape 1 : fonction anonymous_sorries(path) retournant la liste des noms de déclarations fautives. Étape 2 : l’appliquer aux modules — le résultat attendu sur ce lake est une liste courte.
# Exercice a completer : detecteur de sorries anonymesdef anonymous_sorries(path):# retourne la liste des declarations portant un sorry sans mur nomme# ni commentaire d'explication a proximitereturnNone# TODO etudiantpass
Références
Lake : knot_lean/ — README (état des sorries, corridor Reidemeister #8696, bi-implication R1 #11227)
Piccirillo (2020), The Conway knot is not slice, Annals — via Lean-17 §3
Lidman (2026), unknotting number de 11n102 — via Lean-17 §5
Conclusion
Le lake knot_lean n’est pas un décor : des déclarations réelles, une dette de preuve ciblée (des sorries réels, documentés hors-portée Mathlib), une chaîne 3-colorabilité décomposée en bras et murs nommés, un miroir i18n byte-identique. Le compagnon mesure ce que Lean-17 raconte : la formalisation avance en discipline — chaque mur est un théorème, chaque sorry restant est nommé et localisé.