Repository navigation
lean(confiance,#14468): Lean-35 — ce qui rend une preuve formelle fiable (vacuité, axiomes, certificat-vs-headline) — piste Dougherty/von Hippel 2026 #17520
Description
Fille de #14468 (réservoir curé, piste Confiance et preuves)
Source archivée : G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2026 - Dougherty von Hippel - Lies Damned Lies and Proofs - Formal Methods are not Slopless.pdf (blog Secure Program Synthesis, 2026-01-12, 10 p., lu intégralement 2026-09-23). Licence OA (blog + commentaires), exemplaire unique au gisement, aucune copie dans le dépôt.
Gap revalidé sur main (firsthand, 2026-09-23)
- Grep
slop|TCB|vacuité|vacuity|fidélité d'énoncésurMyIA.AI.Notebooks/SymbolicAI/Lean/*.ipynb: aucun notebook de la série ne porte la thématique « ce qui fait qu'on peut se fier à une preuve formelle ». Lean-24-Calibration-Native-Companion parle des axiomes au sens du compte (11 mentions) — pas de vacuité, pas de tête-TCB, pas de fidélité d'énoncé. - Les instruments de contrôle existent déjà dans le dépôt et seront l'organe de vérification (organ-first) :
scripts/lean/count_code_sorry.py(compte réel),proof-integrity/LeanVerifier (check_axioms, classesforbidden:sorryAx,native_decide.*,Classical.choice), le wrapper kernellean4-wsl(v6,find_lake_root— stub~/lean-projects/notebook_contextMathlib 4.32.1 vérifié).
Cible
Nouveau carnet MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-35-Confiance-Preuves-Native.ipynb (prochain numéro libre après 34, kernel lean4-wsl). Exécuté de bout en bout (C.2), ≥3 exercices (C.1, stubs sans erreur volontaire).
Thème : les modes de « slop » formel de la source, rendus exécutables et mesurés avec les vrais instruments du dépôt :
- Preuve triviale par mis-définition (source p.4 : « it's very common that you mis-define some concept such that the proof is accidentally trivial ») — construire un énoncé qui se prouve sans travail (∃ à partir d'une définition qui transporte la conclusion), et le détecter : la preuve est vide, le compte de preuve ne dit rien de la difficulté. Contre-exercice : raffiner la définition pour que l'énoncé redevienne non-trivial.
- Axiomes de secours (p.6, "proofs of false") :
sorry→sorryAx(transitif, invisible à ungrep sorrynaïf),native_decide(réduction native sans preuve) — démontrer les trois classesforbiddenavec#print axiomssur de vrais exemples, et le fait qu'unFalseprouvé implose la théorie (absurd). - Fidélité d'énoncé / certificat-vs-headline (p.4-5) : un théorème est un certificat de SA formulation ; déclarer la vadrouille « X prouvé » alors que la formulation affaiblie (terminaison supposée, égalité d'énoncé ≠ égalité de sémantique) est le défaut central — exercice : apparier énoncés Lean et claims vulgarisés, et montrer que
#print axiomsne dit rien de la fidélité de l'énoncé (orthogonalité des deux axes : axiomes ↔ fidélité).
Acceptance (falsifiable)
- Papermill end-to-end vert (kernel
lean4-wsl, stub lake), outputs committés, exec_counts partout (C.2). - ≥3 exercices, stubs
pass/printsansraise(C.1). - Les 3 classes
forbiddendémontrées vivantes (une cellule par classe, avec sortie#print axiomsréelle citant le nom de l'axiome) + la cellulesorryAxtransitif. - Verdict écrit dans la PR : chaque exercice relie à la page de la source (p.4/p.6/p.4-5).
- Aucun
sorryrésiduel — mesuré parcount_code_sorry.py --json(distinct_code_sorry), pas par grep.
Coût
~1 session notebook (markdown + cellules Lean courtes, stub lake déjà chaud sur la machine d'exécution), aucune nouvelle dépendance, CPU-only.
Activity
jsboige commentedon Sep 23, 2026
Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA — prev: DEEP/notebook-python #17511
[CLAIMED] #17520 — lane myia-po-2027:CoursIA — notebook Lean-35 « Confiance et preuves » (vacuité, axiomes, certificat-vs-headline), source Dougherty/von Hippel 2026 lue intégralement, instruments proof-integrity du dépôt comme organe
paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-35*, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
jsboige commentedon Sep 23, 2026
[DELIVERED] lane myia-po-2027:CoursIA — clôture du grain : PR #17530 (branch
feature/lean35-confiance-preuves, commit3eb36f1602b7).Livraison : notebook
Lean-35-Confiance-Preuves-Native.ipynb(série SymbolicAI/Lean, kernellean4-wsl, lakemathlib_examplesv4.33.0) + README de la série à jour (table principale, stats, arbre, durée).Exécution réelle (papermill WSL, 10/10 cellules, 0 erreur) :
execution_count1..10, sorties committées (C.2)[sorryAx](démo section 2.1),[propext, grandVrai._native.native_decide.ax_1](native_decide sur 2^200 ≤ 3^200),[propext, Classical.choice, Quot.sound](trio normal via Classical.em), 0-axiome (False.elim, témoins existentiels)by sorry(C.1, warningdeclaration uses 'sorry'committés — pattern Lean-26/30) ; l'exécution s'est révélée nécessaire :by omegasur¬ DivParVraie 2 3échouait sansrintropréalable — corrigé à la source puis re-exécuté (Stop & Repair)count_code_sorry.py --json→distinct_code_sorry = 0pour le lakemathlib_examples(aucunsorrydans les fichiers.lean; les sorries du notebook sont les stubs + la cellule démo, tous déclarés)paths:de la claim couvert (Lean-35*,README.mdde la série)Acceptance : les 5 critères de #17520 sont couverts par le body de la PR (voir les liens de cellules par section) —
See #17520.docs(lean,#17675): note de numerotation 35/36 + ligne 36 rattachee a …
feat(lean,#16753): Lean-36 — Annexe A de Tegmark (MUH) en kernel natif (
jsboige commentedon Sep 26, 2026
[CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-35*, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
refactor(lean,#17520): Lean-35 -> Lean-24b -- accretion du palier 24 …
fix(lean,#17520): table stats README -- ligne Confiance-Preuves renum…
jsboige commentedon Sep 26, 2026
Mapping de renumérotation (règle 5 #5081, décision #17545 c.07:00Z), livré dans la PR #17530 :
Lean-35-Confiance-Preuves-Native.ipynbLean-24b-Confiance-Preuves-Native.ipynbAccueil : accrétion du palier 24 (Calibration-Native-Companion) — le carnet approfondit la lecture de confiance d'un certificat que Lean-24 ouvre par
#print axioms. Référents balayés : titre du carnet (cellule 0), README série (ligne parcours repositionnée après 24, arbre ligne 479, table stats), metadata papermill (normalisation basename). Aucun autre référent dans le dépôt (git grep Lean-35 : 0 après renommage). Garde L898 : aucune PR ouverte concurrente sur les chemins Lean-35/Lean-24.feat(lean,#17520): Lean-24b fiabilite d'un certificat formel — mis-de…
jsboige commentedon Sep 27, 2026
[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
issue: 17520
verdict: CLOSE
acceptance:
residue: none
open-prs: 0
comments-reviewed: 4
[/CLOSURE PREFLIGHT]
myia-ai-01 commentedon Sep 27, 2026
Fermeture par ai-01 sur dossier tiers [CLOSURE PREFLIGHT] (lane myia-po-2026:CoursIA-3). Gate check_closure_dossier.py rc=0 a 18:50Z le 2026-09-27 ; PRs citees en preuve relues MERGED, aucun commentaire poste apres le dossier, preuves fichier:ligne recoupees sur main par echantillon.