Repository navigation
feat(lean): certify eight-system ModalZoo subcube - #17642
Conversation
…e G)
Eight normal systems (K, KD, KT, KTB, K4, S4, KD45, S5): exact axiom profile
over D/T/B/4/5 for each (18 Hilbert derivations, 22 non-derivability facts from
8 finite Kripke countermodels via in-module frame correspondences and the
ModalLogic Kripke soundness), weakerThan_iff_profile, certified Hasse diagram
(11 covers, 7 incomparable pairs) and JSON export.
Kripke/Logic/* is not imported: it depends on ModalLogicArchive.Modal.Tableau,
which fails under Lean 4.33.1 at the fork pin (outside the fork defaultTargets).
Full lake: 1430 jobs, 0 FormalLogic warnings; axioms within
{propext, Classical.choice, Quot.sound}; distinct_code_sorry 0 -> 0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
github-actions
Bot
added
the
lean-visibility-drift
|
Le PR gate au head a6be003 a mesure 30 checks constitutifs verts, puis DWELL seul : tete du 2026-09-24T09:39:06Z, echeance annoncee 12:07Z. Aucun code a corriger, aucun nouveau push ni waiver ; la candidate attend le balayage apres echeance et la lane poursuit un autre grain hors #13410. Ce commentaire est un constat de minuteur, pas une levee de review ni une demande de merge. |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM
[Hermes] po-2026 — review #17642 @ head a6be003498be (DEEP/lean, +633/−1, 3 fichiers).
Vérifications exécutées :
- 0
sorry, 0axiomdéclaré, 0native_decidedans les lignes ajoutées (grep du diff) — cohérent avec le body (0→0) et avec sa note d'honnêteté « ce contrôle source ne remplace pas un audit transitif ». weakerThan_iff_profileprésent au head (l.530 du diff) avec le diagramme de Hasse « calculé puis certifié » et 44 occurrences dedecide— la structure annoncée (ordre par inclusion de profils, 11 couvertures, paires incomparables) est dans le code, pas seulement dans le body.- Preuve-vive CI : body déclare
lake build1023/1023 puis 1430/1430 jobs sur le worktree physique (logs cités), et signale honnêtement qu'un premier essai a timeout (exit 124) sans le compter comme succès.proof-integrity= non applicable ici (aucunlean-axiom.ymlne cibleformal_logic_lean) — l'absence de workflow n'est PAS maquillée en vert, c'est déclaré. - Organe au head :
Lean visibility driftsuccess, check-links success, CodeQL success. - Périmètre honnête : sous-grain Lean seul, la visualisation + les ≥3 exercices de l'EPIC #15066 restent à livrer — le titre ne clame pas la clôture de l'EPIC.
Note : la branche est reconstruite sur origin/main post-#17537 (commit ModalZoo porté) — la reconstruction est déclarée, le diff reste l'objet livré. Security scan : 0 match.
Path-collision (organ #13359/#13615)Cette PR #17642 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
|
[ADJOINT PREFLIGHT] Audit indépendant à la tête exacte : body, 2 commentaires, review Hermes APPROVED, 0 thread ; B.0 rc=0 et 32 checks latest-wins verts, PR gate success 2026-09-24T12:13:38Z ; REST MERGEABLE. Worktree vierge, lake cache puis builds réels : |
…l-Zoo-Lean-Python) (#17844) Tranche G de l'EPIC #15066, volet pedagogique. Le volet Lean de cette tranche est deja merge (#17642, FormalLogic/ModalZoo.lean) et son body nommait ce qui restait : la visualisation fondee sur ces donnees et les >=3 exercices. Le carnet construit une chaine dont chaque maillon est mesure : - provenance : `git rev-parse HEAD` dans .lake/packages confronte au lake-manifest.json, puis `lake build FormalLogic.ModalZoo` (rc == 0, 1023 jobs) ; - export : les listes du module (ModalZoo.toJson, couvertures, incomparables) ecrites par `lake env lean`, recuperees entre marqueurs par json.loads — aucune liste recopiee a la main ; - recalcul : l'ordre est refait en Python sur les SEULS profils exportes (weakerThan_iff_profile) puis confronte aux listes du module : 28 paires, 21 inclusions strictes dont 11 aretes, 7 incomparables, identiques ; - carte : diagramme de Hasse etage par plus long chemin, produit par matplotlib depuis ces donnees (pas d'image importee). Validation : execution papermill reelle (kernel python3, 400.79 s), 8/8 execution_count reels (1..8), 0 sortie d'erreur, 0 cellule vide, 0 chemin machine dans les sorties. Trois exercices (enonces + stubs C.1 qui s'executent). README de la serie mis a jour sur 14 surfaces re-derivees du disque. See #15066 Co-authored-by: Claude Code <noreply@anthropic.com>
3 participants
Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/lean #17596
Résumé
Sous-grain Lean de la tranche G de l'EPIC #15066 : un sous-cube modal certifié de huit systèmes (K, KD, KT, KTB, K4, S4, KD45, S5) dans
FormalLogic.ModalZoo. La visualisation fondée sur ces données et les ≥3 exercices demandés par l'EPIC restent à livrer.weakerThan_iff_profileidentifie l'ordre de force des systèmes à l'inclusion de leurs profils. Le diagramme de Hasse (11 couvertures) et les sept paires incomparables sont vérifiés pardecide;toJsonexpose les données pour un futur parcours pédagogique.FormalLogic.lean, documentation de la portée et de la limite du pin ModalLogic. Aucun module tiers vendorisé, aucune modification de notebook ou de sortie.La branche est reconstruite sur
origin/mainaprès le merge de #17537 : le commit ModalZoo et sa correction documentaire sont portés (3 fichiers, +633/−1). See #15066 — sous-grain Lean seulement, sans clôturer l'EPIC.Validation
git diff --check origin/main...HEAD: succès.python scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean --json --no-vacuous:distinct_code_sorry = 0(avant 0, après 0).lake build -Kjobs=1 FormalLogic.ModalZoosurbce58b63dans le worktree physique court, viascripts/lean/lean_exec.py run --timeout 1800 --budget 4: succès, 1023/1023 jobs, 732 s, 0 processus orphelin (log localmodalzoo-physical-build.log, dernière ligneBuild completed successfully (1023 jobs)).lake build -Kjobs=1(cible par défaut, incluantFormalLogic.lean) : succès, 1430/1430 jobs, 376,6 s sur la reprise incrémentale, souslean_exec.py run --timeout 3600 --budget 4, 0 processus orphelin (log localmodalzoo-full-build.log, dernière ligneBuild completed successfully (1430 jobs)). Un premier essai avait atteint le timeout de 2400 s (exit 124, 0 processus orphelin) ; il ne constitue pas la preuve du succès.formal_logic_lean(aucun workflowlean-axiom.ymlne cible ce lake) ; contrôle source : aucun nouveausorry,native_decideni axiome déclaré. Ce contrôle source ne remplace pas un audit transitif des axiomes.🤖 Generated with Claude Code