feat(lean,#16543): Lean-8b — programme Erdos et pattern conjecture-as-sorry (pilote narratif #13106)

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #16075

Résumé

Pilote narratif de l'Epic #13106 (« relier le programme Erdős/formal-conjectures à Lean-7b/Lean-8 ») : nouveau notebook natif Lean-8b-Erdos-Formal-Conjectures-Native.ipynb + 3 lignes de README. Troisième pilote de famille distincte vers le critère d'acceptation de l'Epic (≥3 familles) — après le pilote quantique (#15700) et le pilote calculatoire borné (#13194).

Le contenu exécute in-kernel le geste central du projet Google DeepMind Formal Conjectures (arXiv:2605.13171) : une conjecture ouverte formalisée est un théorème au sorry près, et #print axioms est le discriminant :

• EGZ (Erdős–Ginzburg–Ziv 1935) importé de Mathlib (Int.erdos_ginzburg_ziv, pin v4.33.0) — #print axioms = [propext, Classical.choice, Quot.sound], pas de sorryAx ;
• Erdős–Moser restatée à la main (∀ k m, 2 ≤ k → ∑ i ∈ range m, (i+1)^k ≠ (m+1)^k) — #print axioms = [sorryAx], ticket ouvert assumé ;
• témoin calculé : EGZ appliqué sur (0,1,1,2,2) : Multiset (ZMod 3) (le théorème fournit l'existence, {0,1,2} est vérifié séparément par decide) ;
• contrepoint k = 1 : 1 + 2 = 3 prouvé par decide — pourquoi l'hypothèse 2 ≤ k est nécessaire ;
• 3 exercices (pattern 13b : def placeholder + #eval ancres ; l'exo 2 porte un sorry étudiant qui échoit délibérément au pattern de la section 3) ;
• grille de digestion EPIC: Digestion et canonicalisation des mathématiques assistées par IA #13106 : énoncés/garanties, provenance (erdosproblems.com, arXiv, Mathlib), friction documentée (noms préfixés Int./ZMod., olean de feuille à construire, kernelspec per-lake), raccord corpus (Lean-7b/8 — claims Erdős ancrés en fix(lean-notebooks): ground Erdos proof claims #15209, lake discrepancy feat(lean,#12823): P0 lake discrepancy_lean — définitions + conjectures Prop + énoncé Beck-Fiala 2k−1 #12839, Lean-12 sensitivity).

Exécution (H.1)

• Kernel natif lean4-wsl-groth16200 (kernelspec per-lake, pattern feat(notebook-lean,#14871): Percolation-Lean.ipynb — compagnon exécutable du lake percolation_lean #14927), lake miroir WSL pin v4.33.0, oleans EGZ construits pour le run (lake build Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Tactic).
• Papermill end-to-end via wsl_papermill.py : execution_count réels sur 11/11 cellules code, 0 erreur.
• Sorties commitées : les deux #print axioms visibles, decide rendent 0/None/true attendus.

Note sorry (B.1)

La PR ne touche aucun fichier *.lean (notebook + README uniquement) : le comptage lake count_code_sorry.py est inchangé par construction. Le notebook porte exactement 2 occurrences de sorry en cellule, toutes deux délibérées et pédagogiques : la conjecture Erdős–Moser (section 3 — c'est le sujet du notebook) et le stub de l'exercice 2 (ticket ouvert étudiant, même écho). Aucun sorry n'est ajouté à une preuve existante (§D intact).

Naming (règle accretion-numbering)

Première accrétion de la branche Lean-8 → lettre b (la base occupe a, convention mesurée 80/83). Argument pédagogique dans l'issue #16543 : parent = Lean-8-Agentic-Proving, le benchmark formal-conjectures est le terrain des prouveurs agents.

See #16543 (grain), #13106 (Epic, pilote narratif), #15700 (pilote quantique — forme du livrable).

🤖 Generated with Claude Code

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 11
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	2.9s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.4s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16545 (feat(lean,#16543): Lean-8b — programme Erdos et pattern conjecture-as-sorry (pilote narratif #13106)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- chore(catalog): scheduled auto-regenerate (long-lived PR) #15942 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
• terminal -- feat(lean,#15066): Tranche E — Lean-34 calculabilité et limites (arrêt, point fixe, Gödel I/II, Rosser, Tarski, Löb) #16356 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, recouvrement de chemins 50% -- feat(lean,#15066): Tranche E — Lean-34 calculabilité et limites (arrêt, point fixe, Gödel I/II, Rosser, Tarski, Löb) #16356 est deja sur main.
• terminal -- fix(md-tables,#15719): relais g1-residu — lignes vides après tableaux Lean ; Audio écarté (doublon #16411) #16412 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, recouvrement de chemins 50% -- fix(md-tables,#15719): relais g1-residu — lignes vides après tableaux Lean ; Audio écarté (doublon #16411) #16412 est deja sur main.
• terminal -- feat(lean,#16569): Lean-31 — chronologie 7-14 sept. 2026 + GIFs animés de l'écoulement #16577 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, recouvrement de chemins 50% -- feat(lean,#16569): Lean-31 — chronologie 7-14 sept. 2026 + GIFs animés de l'écoulement #16577 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.