Skip to content

pilote FFL: Foundation — verdict d'intégration mesuré (Part of #15066) #15520

Closed
#15563
Closed
pilote FFL: Foundation — verdict d'intégration mesuré (Part of #15066)#15520
#15563

Description

@jsboige
jsboige
opened on Sep 10, 2026

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/readme #15510

Part of #15066 — premier pilote d'intégration FFL recommandé par l'EPIC (ordre #1).

Objectif

Verdict d'intégration mesuré pour FormalizedFormalLogic/Foundation (Apache-2.0, 199 modules Lean, toolchain 4.33.1), sur pin exact.

Protocole (celui de l'EPIC, exécuté intégralement)

  1. fresh clone au commit exact (pin noté dans ce fil) ;
  2. lake exe cache get puis lake build sur le pin déclaré ;
  3. mesurer le graphe d'import de l'API minimale visée par la Tranche A (Propositional/ — validité, satisfiabilité, contre-modèles) ;
  4. tester la compatibilité avec le toolchain CoursIA courant (Mathlib 4.33.1) ;
  5. auditer licence, sorry/axiomes (#print axioms sur les déclarations exposées) et maintenance (derniers commits, issues upstream) ;
  6. rendre le verdict : IMPORTABLE / CONSUMER_PINNÉ / PORT_BORNÉ / RÉFÉRENCE_SEULE.

Seuil de sortie (EPIC)

RÉFÉRENCE_SEULE si l'intégration exige un fork permanent, plus de 3 modules adaptés / 1000 lignes, un nouveau sorry, ou une dépendance non maintenue sans bénéfice pédagogique démontré.

Livrable

Verdict + mesures (temps build, taille, imports, axiomes) sur cette issue et le dashboard. Aucun vendorising dans ce grain — la consommation (si verdict favorable) relève de la Tranche A (#à_lier).

Activity

  1. jsboige commented on Sep 10, 2026

    @jsboige
    jsboige
    on Sep 10, 2026
    OwnerAuthor

    Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/readme #15510

    [CLAIMED] lane myia-po-2024:CoursIA — exécuter le protocole pilote 1→6 de l'EPIC (clone au pin, cache+build, graphe d'import Propositional, compat toolchain, audit licence/sorry/axiomes, verdict). Fenêtre bornée A (#15440) en parallèle — le build local sera niced pour ne pas fausser le timing du run CI.

  2. jsboige commented on Sep 11, 2026

    @jsboige
    jsboige
    on Sep 11, 2026
    OwnerAuthor

    [CLAIMED-AMEND] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/**, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-3b-*.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md -- le claim couvre le protocole pilote 1-6 (verdict CONSUMER_PINNE livre sur ce fil) ET le pilote consommateur qui le prouve (lake formal_logic_lean + notebook 3b + README), suite a l'arbitrage ai-01 du 2026-09-11T04:31:50Z

  3. jsboige commented on Sep 11, 2026

    @jsboige
    jsboige
    on Sep 11, 2026
    OwnerAuthor

    [LIVRAISON] Verdict d'intégration FFL Foundation — CONSUMER_PINNÉ au pin 81810b9f22c49fbb32bd89c1e9737059d83a37e6. Protocole EPIC 1→6 exécuté intégralement :

    Mesures

    # Étape protocole Résultat mesuré
    1 Clone au pin exact rev 81810b9f vérifiée dans le lake-manifest.json du lake consommateur
    2 cache get + lake build Mathlib ooleans livrés par le cache (5,7 GiB) ; Foundation ne publie pas d'oleans sur le cache leanprover → 877 modules compilés from source, ~20 min (LAKE_JOBS=2), succès
    3 Graphe d'import API minimale (Propositional/ — validité, satisfiabilité, contre-modèles) fermeture 17 modules
    4 Compat toolchain CoursIA v4.33.1 = Mathlib v4.33.1 exact (rev 0df444a360ea) — zéro adaptation
    5a Licence Apache-2.0 (SPDX vérifié)
    5b sorry distinct_code_sorry (count_code_sorry.py) sur le module consommateur : 0
    5c Axiomes #print axioms sur les 5 théorèmes du pont (ci-dessous) : zéro sorryAx, zéro native_decide — 3 théorèmes sur les axiomes standard Lean seulement, la dérivation sur aucun
    5d Maintenance dernier commit au pin 2026-09-10 (PR upstream #921) ; push le plus récent 2026-09-11T04:02Z ; 33 issues ouvertes — dépôt très actif

    #print axioms (pont FormalLogic.Bridge)

    'FormalLogic.Bridge.peirce_valid' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.Bridge.or_not_valid' depends on axioms: [propext, Quot.sound]
'FormalLogic.Bridge.or_satisfiable' depends on axioms: [propext, Quot.sound]
'FormalLogic.Bridge.valuations_exhaustive' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.Bridge.peirce_provable' does not depend on any axioms

    Classical.choice provient du by_cases de l'exhaustivité (attendu) ; la
    dérivation peirce_provable est axiomatiquement vide — le versant preuve est
    purement syntaxique, exactement ce que l'arc pédagogique veut montrer.

    Verdict : CONSUMER_PINNÉ

    Justification :

    • compat toolchain exacte (aucun patch, aucune bifurcation) ;
    • API Propositional/ auto-suffisante pour la Tranche A (validité/satisfiabilité/contre-modèles + métathéorèmes Tait.soundness/completeness! consommables) ;
    • consommation par require foundation @ <pin> dans un lake dédié — zéro vendorising, zéro module adapté, zéro sorry ajouté (seuil RÉFÉRENCE_SEULE non atteint sur tous ses critères) ;
    • maintenance upstream active (jour-1 au pin).

    Coût d'exploitation à connaître : chaque worktree neuf paie la compilation from-source de Foundation (~20 min) puisque le cache leanprover ne la sert pas — le lake consommateur dédié (.lake persistant par worktree) amortit ce coût entre itérations (élaboration du pont : 214 s à chaud, 451 s sous charge CI).

    La PR du premier consommateur (lake formal_logic_lean + notebook Lean-3b + README) suit sur ce fil.

  4. jsboige commented on Sep 11, 2026

    @jsboige
    jsboige
    on Sep 11, 2026
    OwnerAuthor

    [LIVRAISON] PR #15563 — le premier consommateur du verdict : lake formal_logic_lean (CONSUMER_PINNÉ au pin) + notebook Lean-3b-Formalized-Formal-Logic.ipynb + README série (3 insertions). Validation : lake build SUCCESS (214 s / 878 jobs), #print axioms 5/5 (0 sorryAx, 0 native_decide, peirce_provable sans aucun axiome), papermill 22/22 cellules 0 erreur, contre-modèle Tweety p=F,q=F = témoin certifié valFF. Closes la partie consommateur de ce pilote ; l'EPIC #15066 reste ouvert (Tranche A po-2026 sur #15521, Tranches B/C à venir).

  5. myia-ai-01
    added a commit that references this issue on Sep 11, 2026

    feat(lean,#15520): lake formal_logic_lean (FFL CONSUMER_PINNE) + note…

    03b41c7
  6. myia-ai-01
    closed this as completedin #15563on Sep 11, 2026
  7. jsboige
    added 2 commits that reference this issue on Sep 19, 2026

    fix(tweety,#16877): rewrap cellule Lecture pins — «#15520» en debut d…

    c34d5e8

    test(guard,#17005): TestHeadingContinuation — pilote + post-fix + no-…

    5d2c0e0
  8. myia-ai-01
    added 2 commits that reference this issue on Sep 21, 2026

    fix(guard,#17005): detect heading-style rendering of list/blockquote …

    3d6ec6f

    feat(tweety,#15066): laboratoire FOL Tweety vers certificats Lean (#1…

    38f0d27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions