Lean - Solveur mathématique et Vérification Formelle
← SemanticWeb | ↑ SymbolicAI | Planners →
Cette série introduit Lean 4, un assistant de preuves et langage de programmation fonctionnel basé sur la théorie des types dépendants. Le fil rouge va des fondations (types dépendants, mode tactique, Mathlib) vers l’état de l’art : assistance aux preuves par LLM et vérification formelle de réseaux de neurones, ports de théorèmes phares (théorème de Kochen-Specker / 18 vecteurs Cabello ; théorème du libre arbitre de Conway-Kochen ; finitude des dérivées symboliques de Brzozowski), théorie des nœuds (mouvements de Reidemeister, tricolorabilité de Fox, noeud de Conway et preuve de Piccirillo), hommages aux mathématiciens (Grothendieck et le langage grothendieckien dans Mathlib 4 ; John Conway, l’homme et l’oeuvre), et théorie de la décision (cohérence de de Finetti : le Dutch book comme témoin d’une incohérence).
Aperçu — Lean en images
Six visualisations extraites des notebooks illustrent l’arc de la série : de l’assistance aux preuves par LLM et la vérification formelle de réseaux de neurones jusqu’aux automates de Conway (Game of Life) et à la théorie des nœuds (nœuds simples, couple de mutants Conway/Kinoshita-Terasaka, invariant d’Alexander). Provenance détaillée : MANIFEST.md.
Assistance aux preuves et vérification formelle
L’état de l’art de la série : un LLM génère des preuves Lean, dont on mesure la performance sur un banc de théorèmes (Lean-7b), puis TorchLean propage intervalles (IBP) et bornes (CROWN) pour certifier formellement la robustesse d’un réseau de neurones (Lean-11b).
Conway — Game of Life
L’hommage à John Conway passe par le Game of Life comme modèle de calcul (Lean-16b), où Lean sert de certificat pour les structures et leurs périodes.
Théorie des nœuds
La série dédiée (companion knot_lean, Epic #2874) développe trois vues complémentaires : les nœuds les plus simples classés par nombre de croisements (Lean-17a), le couple de mutants Conway (11n34) / Kinoshita-Terasaka (11n42) dont Lisa Piccirillo prouva que seul le second borne un disque lisse (slice), puis le polynôme d’Alexander — trivial (= 1) pour ce couple, et donc incapable à lui seul de distinguer leur sliceness (Lean-17b).
Modes d’exécution suggérés
| Mode | Notebooks | Temps | Description |
|---|---|---|---|
| Fondations | 1-5 | ~3h | Base théorique complète (types, logique, tactiques) |
| Avec Mathlib | 1-6 | ~3h45 | Ajoute les tactiques Mathlib |
| Intégration IA | 1-7, 7b | ~5h | Ajoute LLMs, exemples et benchmarks |
| Complet | 1-12 | ~11h | Toutes les fonctionnalités incluant LeanDojo et théorème de sensibilité |
| Avec Pilier 1.B | 1-12, 13 | ~12h | Inclut le port Kochen-Specker (Cabello 18-vecteurs) - contextuality quantique |
| Avec hommages | 1-12, 13, 15, 16a, 16b, 16c, 16d, 16e, 16f, 16g, 16h, 16i, 16j | ~20h10 | Ajoute Lean-15 (Grothendieck), Lean-16a (Conway, l’homme et l’oeuvre), Lean-16b (Conway, Game of Life), Lean-16d (Conway, Game of Life sur kernel Lean natif), Lean-16e (Conway, FRACTRAN sur kernel Lean natif), Lean-16f (Conway, théorème du libre arbitre - adossé à Lean-13), Lean-16g (Conway, canons - le barreau 2 de l’échelle des témoins Life), Lean-16h (tournée des motifs sur kernel natif), Lean-16i (translateur minuscule, Loi II) et Lean-16j (correction Hashlife sur kernel natif) |
| Avec théorie des nœuds | 1-12, 13, 15, 16a-c, 16f, 17a, 17b | ~17h30 | Ajoute Lean-17a (Conway, les nœuds et la preuve de Piccirillo) et Lean-17b (invariants : PD-codes, tricolorabilité de Fox, mouvements de Reidemeister) - companion knot_lean, Epic #2874 |
Structure
Partie 1 : Fondations (basé sur PDF de référence)
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 1 | Lean-01-Setup-Lean-Python | Installation elan, kernel Jupyter, vérification | 15 min |
| 2 | Lean-02-Dependent-Types-Lean | Calcul des Constructions, types, polymorphisme, déclarer ses propres types (inductive, structure, deriving) |
40 min |
| 3 | Lean-03-Propositions-Proofs-Lean | Prop, connecteurs, Curry-Howard, preuves par termes | 45 min |
| 3b | Lean-03b-Formalized-Formal-Logic-Lean-Python | Pont Tweety ↔︎ Lean : les mêmes formules exécutées par le raisonneur et certifiées par le noyau (table par mondes possibles, validité/contre-modèle/preuve, métathéorèmes Tait consommés) - companion du lake formal_logic_lean (Foundation piné, Epic #15066) |
45 min |
| 4 | Lean-04-Quantifiers-Lean | forall, exists, égalité, arithmétique Nat | 40 min |
| 5 | Lean-05-Tactics-Lean | Mode tactique, apply/exact/intro/rw/simp | 50 min |
Partie 2 : État de l’art et intégration IA
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 6 | Lean-06-Mathlib-Essentials-Lean | Mathlib4, tactiques ring/linarith/omega, recherche | 45 min |
| 7 | Lean-07-LLM-Intégration | LeanCopilot, AlphaProof, patterns LLM-Lean | 50 min |
| 7b | Lean-07b-Examples-Python | Exemples progressifs, benchmarks, cas pratiques | 40 min |
| 8 | Lean-08-Agentic-Proving-Python | Agents autonomes, APOLLO, problèmes Erdos | 55 min |
| 8b | Lean-08b-Erdos-Formal-Conjectures-Lean | Companion natif (kernel Lean) : le programme Erdős et le pattern conjecture-as-sorry — EGZ importé de Mathlib (#print axioms = [propext, Classical.choice, Quot.sound]), équation d’Erdős–Moser restatée ([sorryAx] visible), témoin calculé dans ZMod 3 - pilote narratif Epic #13106 |
25 min |
| 9 | Lean-09-SK-Multi-Agents-Lean-Python | Agent Framework (Microsoft), orchestration multi-agents | 45 min |
| 10 | Lean-10-LeanDojo | LeanDojo: tracing, theorems, Dojo interactif | 45 min |
| 10b | Lean-10b-LeanDojo-v2-Pantograph-Lean-Python | LeanDojo-v2 : base dynamique (DynamicDatabase, curriculum random/novel_premises), serveur RPC Pantograph (but → tactique → état, pas à pas et preuve entière check_compile), pipeline « tracage → politique → vérification Lean » qui réalise l’exercice 3 de Lean-10 - See #18430 |
40 min |
| 11 | Lean-11-TorchLean | TorchLean: réseaux de neurones vérifiés, IBP, CROWN | 1h30-2h |
| 11b | Lean-11b-TorchLean-Python | Implémentation Python des algorithmes de vérification (IBP, CROWN) | 1h30-2h |
| 12 | Lean-12-Sensitivity-Theorem | théorème de sensibilité (Huang 2019), hypercube, signing matrix, port Lean 4 | 60 min |
| 12b | Lean-12b-Lean-Sensitivity-Theorem | Companion natif (kernel Lean) : preuve formelle 0-sorry de Huang dans le lake sensitivity_lean, #check + #print axioms rendus in-kernel (UNLOCK c.127, jonction Mathlib #2611) |
45 min |
Partie 3 : théorèmes phares (ports complets)
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 13 | Lean-13-Kochen-Specker | théorème de Kochen-Specker (1967), preuve Cabello 18 vecteurs, parité, contextuality quantique - Pilier 1.B Epic #1651 | 60 min |
| 13b | Lean-13b-CHSH-Tsirelson-Native | Companion natif du lake conway_lean : la borne de Tsirelson exécutée in-kernel — #check de la signature exacte (7 classes de types + IsCHSHTuple, conclusion ≤ (2 * √2) • 1), #print axioms = [propext, Classical.choice, Quot.sound] sans sorryAx, frontière classique mesurée (score 2 atteint, mélange équilibré → 0), contrôle positif de kernel contre le REPL muet (#11874) et 3 exercices - Epic #13106 |
30 min |
| 13c | Lean-13c-CHSH-Landau-Saturation | Companion natif du lake conway_lean : la saturation de Tsirelson exécutée in-kernel — #check de l’égalité centrale chshOperator A₀ A₁ B₀ B₁ = (2 * √2) • 1 (égalité exacte, pas un majorant : la borne de Lean-13b devient un maximum démontré), #print axioms = [propext, Classical.choice, Quot.sound] sans sorryAx, témoin de Pauli (sigmaZ, sigmaX, B₀, B₁ en Matrix (Fin 2) (Fin 2) ℝ), forme spectrale bilatérale (2√2 sur la diagonale), anticommutateur, critère de Landau vérifié sur le témoin (spectre ±1) et 3 exercices - Epic #13106 |
25 min |
| 13d | Lean-13d-CHSH-Indeterminisme-Native | Companion natif du lake conway_lean : la route statistique vers l’indéterminisme exécutée in-kernel — modèle local déterministe du jeu CHSH en vocabulaire FWT (AliceResponse/BobResponse : fonctions de l’état caché, localité par signature, l’analogue structurel de MIN), frontière locale état par état (|realizedScore| = 2, délégué à classical_abs_score), écart de Tsirelson 2 < 2√2 et conclusion chsh_indeterminism (aucun modèle local déterministe ne réalise un score > 2 en réels — la même conclusion que le théorème du libre arbitre, obtenue par l’argument statistique), tableau comparatif des deux routes (contextuelle vs statistique) et 3 exercices - Epic #13106 |
25 min |
| 14 | Lean-14-Finiteness-Derivatives | Dérivées symboliques de Brzozowski : la finitude des dérivées qui garantit le matching linéaire (langages rationnels, automates) | 25 min |
| 14b | Lean-14b-Finiteness-Lean-Companion | Companion natif (kernel Lean) : les 7 déclarations du lake finiteness_lean (Regex, nullable, deriv, derivWord, accepts, aStar, abWord) re-déclarées fidèlement (kernel sans oleans), vérifiées et exécutées in-kernel, finitude observée sur une regex à union (6 préfixes → 4 dérivées distinctes) |
20 min |
Partie 4 : Hommages mathématiciens
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 15 | Lean-15-Grothendieck-Tribute | Langage grothendieckien dans Mathlib 4 : catégories/foncteurs, cribles et topologies de Grothendieck, faisceaux, schémas, site de Zariski, morphismes étales/lisses - Epic #1646 | 45 min |
| 15b | Lean-15b-Lean-Grothendieck | Atelier pratique Grothendieck : cribles, topologies et faisceaux en exercices (compagnon grothendieck_lean, fait suite à Lean-15) - Epic #1646 |
50 min |
| 15c | Lean-15c-Lean-Grothendieck-Companion | Companion formel natif du lake grothendieck_lean en kernel lean4-wsl : les 51 modules visités par leurs énoncés qui compilent (Yoneda, forme flèche Covers*, faisceautisation, Čech, Mayer-Vietoris, Zariski), 0 sorry attesté par #print axioms - Epic #11703 |
40 min |
| 15d | Lean-15d-Lean-Grothendieck-Visuel-Python | Visite guidée visuelle des abstractions grothendieckiennes : sept figures Python autonomes (catégories et foncteurs, cribles, topologie de Grothendieck, faisceaux, Yoneda, site de Zariski, synthèse) et trois exercices sur données manipulables (fermeture d’un crible, compatibilité d’une famille de sections, critère de recouvrement par le pgcd) — aucun kernel Lean requis - See #17978 | 35 min |
| 16a | Lean-16a-Conway-Man-and-Work | Conway, l’homme et l’oeuvre : biographie et style singulier (le jeu comme méthode) ; panorama des grands résultats (nombres surréels, groupes de Conway & Monstrous Moonshine, réseau de Leech, polynôme de Conway, Doomsday, Look-and-Say, FRACTRAN, problème de l’Ange, Sprouts, théorème du libre arbitre) ; premières noix crackées exécutées depuis conway_lean (Doomsday, Look-and-Say, Nim, Angel, Life - 0 sorry) - Epic #1647 / #2154 | 50 min |
| 16b | Lean-16b-Conway-Game-of-Life-Lean | Hommage à John Conway : Game of Life as Computation, Doomsday, FRACTRAN, Look-and-Say, Nim, Angel - Epic #1647 | 60 min |
| 16c | Lean-16c-Conway-Game-of-Life-Golly | Game of Life : les 3 piliers en images (compagnon Golly, intégration CLI bgolly pour simulation certifiée) - Epic #1647 |
45 min |
| 16d | Lean-16d-Conway-Game-of-Life-Lean-Native | Game of Life sur kernel Lean natif (lean4-wsl) : grille, règle B3/S23, moteur step/evolve, motifs (bloc, clignoteur, planeur) et faits certifiés par decide/native_decide, sans axiome sorry - Epic #1647 / #3294 |
40 min |
| 16e | Lean-16e-Conway-FRACTRAN-Lean-Native | FRACTRAN sur kernel Lean natif (lean4-wsl) : type Frac (preuve den > 0), moteur fracMulNat/fractranStep/fractranRun, programmes (doubler, diviser) et le générateur de nombres premiers de Conway (14 fractions), faits certifiés par decide sans axiome sorry - Epic #1647 / #3294 |
40 min |
| 16f | Lean-16f-Conway-Free-Will-Theorem | théorème du libre arbitre (Conway-Kochen) : les trois axiomes SPIN/TWIN/MIN en profondeur, argument en deux temps (1 particule via Kochen-Specker, puis 2 particules via TWIN), ce que le théorème dit et NE dit PAS, port formel adossé à FreeWillTheorem.lean (chaîne de réduction free_will_theorem -> fwt_single_particle -> kochen_specker, 0 sorry), registre d’extensibilité - Epic #2162 / #2156 |
40 min |
| 16g | Lean-16g-Conway-Canons | Barreau 2 de l’échelle des témoins Life (#12223, chantier #12205) : la source périodique (canon de Gosper) — reconnaître (période 30, transitoire 0, cadence d’émission 30 mesurées), générer (recherche bornée 3 000 soupes, zéro calibré par contrôle positif), certifier (prédicat core (evolve 30 gosper_gun) = core gosper_gun évalué #eval sur horizons 30/60/90 depuis le lake), barreaux 3-4 nommés hors d’atteinte |
45 min |
| 16h | Lean-16h-Conway-PatternTour-Native | La tournée des motifs du Jeu de la Vie en compagnon formel natif (kernel lean4-wsl) : les théorèmes de Conway.Life.PatternTour importés et exécutés in-kernel (still lifes, oscillateurs, vaisseaux — égalités Bool réduites par le noyau, #print axioms en transparence) - Epic #11703 |
40 min |
| 16i | Lean-16i-Translateur-Life | Synthèse d’un translateur minuscule : franchir la Loi II (recoordonner, passer du vérificateur au constructeur) — énumération SAT sur grille bornée du motif T (vitesse (2,-2), période 8), sérialisation JSON vers Lean - Grain B1 du Chantier 2 #12205 | 40 min |
| 16j | Lean-16j-Conway-Hashlife-Correctness-Native | Compagnon formel natif (kernel lean4-wsl) des modules de correction Hashlife de conway_lean : cône de lumière (chebDist, lightCone_subset_of_le), MacroCell (niveaux, emptyOfLevel), les 4 murs NE/NW/SW/SE (p4_*_membership_arm), théorème de marge (hashlife_correct_margin + contre-exemples cexBlock1), GridCanonical, batterie adverse, DecideProbe, Novelty — imports exécutés in-kernel, transparence axiomatique #print axioms - Epic #11703 |
45 min |
Partie 5 : Théorie des noeuds
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 17a | Lean-17a-Knots-Conway-Proofs | Conway, les nœuds et la preuve de Piccirillo : le noeud de Conway (11n34), slice-genre et nombre de dénouement, contexte de la preuve (Piccirillo 2020, le noeud de Conway n’est pas slice) - hommage narratif, Epic #2874 | 40 min |
| 17b | Lean-17b-Knots-Invariants-Companion | Invariants de nœuds : PD-codes, mouvements de Reidemeister, tricolorabilité de Fox, diagrammes bien formés - companion knot_lean (Epic #2874, transfer forward #3000 sorry-free + backward #3124 partiel) |
60 min |
| 17c | Lean-17c-Knots-Companion-Formel | Companion formel du lake knot_lean en kernel python3 (kernel lean4-wsl gelé #11874) : les modules que Lean-17 ne cite pas (Basic, Invariant, Reidemeister) interrogés par leurs déclarations réelles, murs nommés R2/R3, sorries réels (14) vs prose, miroir i18n byte-identique attesté par l’instrument canonique - Epic #2874 / #11703 |
40 min |
Partie 6 : Recherche pondérée et optimalité (A*)
| # | Notebook | Contenu | Durée |
|---|---|---|---|
| 18 | Search-03e-AStar-Optimality | Optimalité de A* sous heuristique admissible : graphe pondéré ℝ≥0 et coût additif pathCost, prédicats Admissible/Consistent, théorème phare admissible_le_suffix_cost (borne en f), téléscopage consistent_implies_path_bound + monotonie de f - companion search_lean (lake Search/, 0 sorry, registre #3801 prong B) |
35 min |
Acquis d’apprentissage
A l’issue de la série, vous saurez :
Modéliser un raisonnement mathématique dans le Calcul des Constructions : types dépendants, univers, propositions comme types (Curry-Howard). Notebooks 2-3 ancrent ces objets sur des exemples concrets (Vector, propositions logiques) plutôt que sur de l’abstraction nue.
Prouver un théorème en mode tactique avec les briques Mathlib :
intro/apply/exact/rflpour la structure,ring/linarith/omega/simppour l’arithmétique et la simplification,induction/cases/rcasespour l’analyse de cas. Notebooks 4-6.Intégrer un LLM au workflow de preuve : patterns LeanCopilot et AlphaProof (n-best, MCTS), prompts goal-aware, comparaison ND-search vs CoT, agents APOLLO/Erdos — fiables surtout sur les preuves courtes, limites persistantes sur les preuves longues et la couverture Mathlib (usage en assistant, pas en oracle). Notebooks 7-9.
Tracer et explorer une base de preuves à grande échelle : LeanDojo (parsing AST, theorem extraction, interaction Dojo), réseaux de neurones vérifiés via IBP/CROWN (TorchLean). Notebooks 10-11.
Porter un théorème de recherche en Lean 4 : théorème de sensibilité (Huang 2019, hypercube et signing matrix), théorème de Kochen-Specker (Cabello 18 vecteurs, argument de parité, contextuality quantique). Notebooks 12, 13.
Lire le langage grothendieckien dans Mathlib 4 : catégories et foncteurs, cribles et topologies de Grothendieck, faisceaux, schémas et sites, morphismes étales/lisses — comme entrée vers la géométrie algébrique formalisée. Notebook 15.
Situer l’oeuvre de Conway dans sa largeur : des nombres surréels au Monstrous Moonshine, du réseau de Leech au théorème du libre arbitre, en exécutant les premières noix formalisées (Doomsday, Look-and-Say, Nim, Angel, Life) directement depuis le projet conway_lean (0 sorry). Notebook 16a.
Explorer les noix de Conway en Lean 4 : Game of Life as Computation, Doomsday, FRACTRAN, Look-and-Say, Nim, Angel — port formel de résultats combinatoires iconiques. Notebooks 16a-16e.
Comprendre le théorème du libre arbitre (Conway-Kochen) : les axiomes SPIN/TWIN/MIN, l’argument en deux temps qui réduit le cas à deux particules au théorème de Kochen-Specker (Notebook 13), et la lecture honnête de sa portée (ce qu’il dit et ne dit pas) — adossé à
FreeWillTheorem.lean(0 sorry). Notebook 16f.Franchir un barreau de l’échelle vérifier→construire : reconnaître une source périodique Life (période, transitoire, cadence d’émission mesurées sur le canon de Gosper), chercher à en générer une dans un budget borné (zéro calibré par contrôle positif), et certifier la périodicité du noyau par un prédicat
Gridévalué sur horizon fini — l’écart structurel entre vérificateur et constructeur. Notebook 16g.Formaliser les invariants de nœuds : PD-codes, mouvements de Reidemeister et tricolorabilité de Fox, en s’appuyant sur le companion
knot_lean(transfert de tricolorabilité le long d’un twist R1 connecté, preuve forward sorry-free + backward partielle). Notebooks 17a, 17b.Lire le paysage galoisien moderne : la preuve formelle que M₂₃ (groupe sporadique de Mathieu d’ordre 10 200 960) est simple est vendored dans le companion
galois_lean/(PR #10486, août 2026, Apache-2.0) ; la réalisation galoisienne — M₂₃ groupe de Galois sur ℚ — est prouvée dans le préprint (Huang–Jackson–Lee–Poonen–Pries–Zhang, arXiv:2608.08538, 9 août 2026 : polynôme explicite f₁ de degré 23, identification23T5) mais non formalisée — le notebook Lean-22 exécute la preuve formelle côté groupe et vérifie f₁ computationnellement, les deux énoncés soigneusement distingués (Epic #10478).Construire le témoin d’une incohérence : le Dutch book de de Finetti — si les prix violent l’inclusion-exclusion, un livret (+1,+1,−1,−1) encaisse l’écart uniformément dans tous les états (miroir exact du lake
decision_theory_lean, arithmétique exacteFraction), et un balayage borné certifie l’absence de livre sur le système réparé ; symétriquement, seule la transformation affine d’une utilité vNM préserve les préférences (0 divergence) quand le carré en fabrique (124 sur les 2145 paires de 66 loteries). Notebook 25.Séparer exposition et vérification d’un résultat formel profond : relire les chaînes Euler/BKM et les deux adaptateurs Navier–Stokes sans confondre leur portée mathématique avec l’acceptation mécanique, puis re-dériver un verdict fail-closed depuis huit termes indépendants — identité, dépendances, toolchain, confinement, axiomes, intégrité et deux gates exacts. Notebook 31.
Pour l’état formel détaillé des modules support (preuves résolues vs sorry résiduels), voir LEAN_INVENTORY.md, le README du projet conway_lean, et le README du projet grothendieck_lean.
Statut de maturité
| # | Notebook | Cellules | Exercices | Solutions | Statut |
|---|---|---|---|---|---|
| 1 | Setup | ~17 | - | - | COMPLET |
| 2 | Dependent-Types | ~50 | 3 | 3 | COMPLET |
| 3 | Propositions-Proofs | ~50 | 3 | 3 | COMPLET |
| 3b | Formalized-Formal-Logic | ~22 | 3 | 0 | NOUVEAU (kernel python3 + lake formal_logic_lean, Epic #15066) |
| 4 | Quantifiers | ~46 | 3 | 3 | COMPLET |
| 5 | Tactics | ~70 | 3 | 3 | COMPLET |
| 6 | Mathlib-Essentials | ~45 | 3 | 3 | COMPLET |
| 7 | LLM-Intégration | ~50 | 2 | 2 | COMPLET |
| 7b | Examples | ~40 | 3 | 3 | COMPLET |
| 8 | Agentic-Proving | ~70 | 2 | 2 | COMPLET |
| 8b | Erdos-Formal-Conjectures (natif) | ~4 | 3 | 0 | NOUVEAU (kernel lean4-wsl-groth16200, Epic #13106) |
| 9 | SK-Multi-Agents | ~50 | 2 | 2 | COMPLET |
| 10 | LeanDojo | ~100 | 2 | 0 | COMPLET |
| 11 | TorchLean | ~40 | 3 | Oui | COMPLET |
| 11b | TorchLean Python | ~45 | 3 | Oui | COMPLET |
| 12 | Sensitivity-Theorem | ~31 | 4 | Non | NOUVEAU |
| 12b | Lean-Sensitivity-Theorem (natif) | ~19 | 3 | 0 | NOUVEAU (kernel lean4-wsl) |
| 13 | Kochen-Specker | ~25 | 1 | 0 | NOUVEAU |
| 13b | CHSH-Tsirelson-Native | ~8 | 3 | 0 | NOUVEAU (kernel lean4-wsl-conway) |
| 13c | CHSH-Landau-Saturation | ~11 | 3 | 0 | NOUVEAU (kernel lean4-wsl-conway) |
| 13d | CHSH-Indeterminisme-Native | ~10 | 3 | 0 | NOUVEAU (kernel lean4-wsl-conway) |
| 14 | Finiteness-Derivatives | ~12 | 1 | - | NOUVEAU |
| 14b | Finiteness-Lean-Companion | ~19 | 3 | 0 | NOUVEAU (kernel lean4-wsl) |
| 15 | Grothendieck-Tribute | ~23 | 0 | - | NOUVEAU (hommage) |
| 15b | Lean-Grothendieck (atelier) | ~40 | 4 | Oui | NOUVEAU |
| 15c | Lean-Grothendieck-Companion | ~25 | 2 | 0 | NOUVEAU (kernel lean4-wsl) |
| 16a | Conway-Man-and-Work | ~39 | 3 | 0 | NOUVEAU (hommage) |
| 16b | Conway-Game-of-Life-Lean | ~26 | 0 | - | NOUVEAU (hommage) |
| 16c | Conway-Game-of-Life-Golly | ~47 | 5 | - | NOUVEAU (hommage) |
| 16d | Conway-Game-of-Life-Lean-Native | ~32 | 3 | 0 | NOUVEAU (hommage, kernel lean4-wsl) |
| 16e | Conway-FRACTRAN-Lean-Native | ~22 | 3 | 0 | NOUVEAU (hommage, kernel lean4-wsl) |
| 16f | Conway-Free-Will-Theorem | ~28 | 3 | 0 | NOUVEAU (hommage) |
| 16g | Conway-Canons | ~23 | 3 | - | NOUVEAU (barreau 2 #12223) |
| 16h | Conway-PatternTour-Native | ~9 | 3 | 0 | NOUVEAU (kernel lean4-wsl, Epic #11703) |
| 16i | Translateur-Life | ~4 | 0 | - | NOUVEAU (grain B1 #12205) |
| 16j | Conway-Hashlife-Correctness-Native | ~15 | 3 | 0 | NOUVEAU (kernel lean4-wsl, Epic #11703) |
| 17a | Knots-a-Conway-and-Proofs | ~13 | 0 | - | NOUVEAU (hommage) |
| 17b | Knots-b-Invariants-Companion | ~19 | 3 | - | NOUVEAU |
| 17c | Knots-Companion-Formel | ~33 | 3 | 0 | NOUVEAU (kernel python3) |
| 18 | Sendov-Complex-Analysis | ~22 | 3 | 0 | NOUVEAU |
| 19 | Analysis-I-Tao-Workflow | ~18 | 3 | 0 | NOUVEAU |
| 20 | PFR-Entropy-Method | ~23 | 3 | 0 | NOUVEAU |
| 20b | PFR-Primitives-Transportables | ~6 | 0 | - | NOUVEAU (digestion #12214) |
| 21 | MIMO-Detection-Flips | ~34 | 6 | 0 | NOUVEAU |
| 21b | MIMO-Converse-Native | ~30 | 0 | - | NOUVEAU (kernel lean4-wsl) |
| 21c | Descente-Budget | ~9 | 8 | 0 | NOUVEAU (#12219) |
| 22 | Galois-Probleme-Inverse-M23 | ~25 | 3 | 0 | NOUVEAU (exécution Lean + sympy) |
| 23 | ERC20-Invariant-Companion | ~21 | 3 | 0 | NOUVEAU (lecture statique Python du lake) |
| 23b | Lean-ERC20-Native-Companion | ~30 | 2 | - | NOUVEAU (kernel lean4-wsl) |
| 24b | Confiance-Preuves-Native | ~10 | 3 | 0 | NOUVEAU (kernel lean4-wsl, lake mathlib_examples, piste Dougherty/von Hippel #14468) |
| 24 | Calibration-Native-Companion | ~27 | 0 | - | NOUVEAU (kernel lean4-wsl) |
| 25 | Coherence-et-Temoin | ~21 | 3 | 0 | NOUVEAU (kernel python3, miroir exact du lake) |
| 26 | Munkres-Tribute | ~9 | 3 | 0 | NOUVEAU (hommage, kernel lean4-wsl) |
| 27 | EdgeColoring-Tutte-Companion | ~10 | 0 | - | NOUVEAU (kernel lean4-wsl, compagnon App-22) |
| 28 | Complex-Structure-S6 | ~28 | 3 | 0 | NOUVEAU (kernel python3, reproduction du dépôt piné) |
| 29 | Hecke-Operators-Native | ~32 | 3 | 0 | NOUVEAU (kernel lean4-wsl, lake hecke_lean) |
| 30 | FormalGroups-Native | ~33 | 3 | 0 | NOUVEAU (kernel lean4-wsl, lake formal_groups_lean) |
| 31 | Euler-Navier-Stokes | 34 | 3 | 0 | NOUVEAU (kernel python3, reproduction pinée et double noyau) |
| 34 | Calculabilite-et-Limites | 19 | 3 | 0 | NOUVEAU (kernel python3 + lake formal_logic_lean, Tranche E Epic #15066) |
| 36 | Structures-Finies-MUH | 23 | 3 | 0 | NOUVEAU (kernel lean4-wsl, lake tegmark_muh_lean, Annexe A de Tegmark) |
Tous les notebooks incluent : - Navigation header/footer avec liens vers notebooks précédent/suivant - Plan de ce Notebook avec liens ancres (notebooks 2-4) - Tableaux récapitulatifs en fin de section - Exercices avec solutions complètes
Quick Start
# 1. Installer elan (gestionnaire Lean)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan default leanprover/lean4:stable
# 2. vérifier l'installation
lean --version # Lean 4.x.x
elan show # toolchain active
# 3. Ouvrir le premier notebook (WSL requis)
wsl -d Ubuntu -- bash -c "jupyter notebook Lean-01-Setup-Lean-Python.ipynb"Pour les notebooks 7-10 (LLM), configurer .env avec OPENAI_API_KEY. Pour le prover daemon, voir section “Prover daemon”.
Prerequisites
- Connaissances de basé en logique mathématique
- Familiarité avec la programmation fonctionnelle (utile mais non obligatoire)
- Pour notebooks 7-8 : compte OpenAI/Anthropic pour APIs LLM (optionnel)
Installation
1. Installer elan (gestionnaire de versions Lean)
# Linux/macOS
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Windows (PowerShell)
Invoke-WebRequest -Uri https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | Invoke-Expression2. Installer Lean 4
elan default leanprover/lean4:stable3. Installer le kernel Jupyter (optionnel)
# Créer un environnement conda
conda create -n lean4-jupyter python=3.10
conda activate lean4-jupyter
# Installer lean4_jupyter
pip install lean4_jupyter
# vérifier l'installation
jupyter kernelspec list4. Configuration API pour notebooks LLM (optionnel)
cd MyIA.AI.Notebooks/SymbolicAI/Lean
cp .env.example .env
# Éditer .env et ajouter OPENAI_API_KEY ou ANTHROPIC_API_KEYRessources externes
Documentation Lean
Mathlib
LLM et Preuves Automatiques
- LeanCopilot
- LeanDojo - ML/LLM theorem proving
- AlphaProof Paper Analysis
- APOLLO System
- Erdos Problems Formalization
LeanDojo
- LeanDojo Documentation
- LeanDojo Paper (NeurIPS 2023)
- lean4-example Repository
TorchLean
Références académiques
| Référence | Couverture |
|---|---|
| de Moura & Ullrich, “The Lean 4 Theorem Prover and Programming Language” (2021) | système Lean 4 |
| The Mathlib Community, “The Mathlib Library” (2020), arXiv:1910.09436 | Mathlib4 |
| Avigad, “Mathematics and Programming” (2024) — Mathematics in Lean | Fondations notebooks 1-5 |
| Jiang et al., “LeanDojo: Theorem Proving with Retrieval-Augmented Language Models” (NeurIPS 2023) | LeanDojo, notebooks 10 |
| First et al., “AlphaProof: Formal Math Reasoning” (DeepMind, 2024) | Notebook 7 |
| Song et al., “Towards Counting Forall: Neural Network Vérification via IBP, CROWN, and LiRPA” | TorchLean, notebooks 11 |
| Geanakoplos, “Three Brief Proofs of Arrow’s Impossibility Theorem” (2005) | Cross-séries GameTheory |
| Sen, “Collective Choice and Social Welfare” (1970) | Cross-séries GameTheory |
Document source
- Notebooks 1-5 basés sur :
D:\Dropbox\IA101\TPs\TP - Z3 - Tweety - Lean.pdf(Section VI) - Notebooks 6-8 basés sur : Recherches état de l’art 2025-2026
Validation
# vérifier la structure des notebooks
python scripts/verify_notebooks.py MyIA.AI.Notebooks/SymbolicAI/Lean --quick
# vérifier l'installation Lean
lean --version
elan showPercées récentes (2024-2026)
| système | Accomplissement |
|---|---|
| AlphaProof (DeepMind) | Médaille d’argent IMO 2024 |
| Harmonic Aristotle | Résolution Erdos #124 variant (~30 ans ouvert) en 6h |
| DeepSeek-Prover | Résolution de problèmes Erdos 379, 987, 730, 198 |
| Mathlib4 v4.31.0-rc1 | 4M+ lignes, utilisé par Terry Tao |
Notes techniques
- Lean 4 (pas Lean 3) - syntaxe moderne
- Preuves constructives + logique classique (via
open Classical) - Progression : termes -> tactiques -> Mathlib -> LLMs -> agents
- Kernel Jupyter : lean4_jupyter (recommandé)
Structure des fichiers
Lean/
├── Lean-01-Setup-Lean-Python.ipynb # Python kernel - diagnostics
├── Lean-02-Dependent-Types-Lean.ipynb # Lean4 kernel
├── Lean-03-Propositions-Proofs-Lean.ipynb
├── Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb # Python kernel - pont Tweety↔Lean (raisonneur + noyau, lake formal_logic_lean, Epic #15066)
├── Lean-04-Quantifiers-Lean.ipynb
├── Lean-05-Tactics-Lean.ipynb
├── Lean-06-Mathlib-Essentials-Lean.ipynb
├── Lean-07-LLM-Integration-Lean-Python.ipynb # Python kernel - APIs LLM
├── Lean-07b-Examples-Python.ipynb # Python kernel - benchmarks
├── Lean-08-Agentic-Proving-Python.ipynb # Python kernel - orchestration
├── Lean-08b-Erdos-Formal-Conjectures-Lean.ipynb # Lean4 (WSL, grothendieck-16200) kernel - pattern conjecture-as-sorry : EGZ Mathlib + Erdős-Moser restatée (Epic #13106)
├── Lean-09-SK-Multi-Agents-Lean-Python.ipynb # Python kernel - Agent Framework
├── Lean-10-LeanDojo.ipynb # Python kernel - LeanDojo
├── Lean-10b-LeanDojo-v2-Pantograph-Lean-Python.ipynb # Python kernel (WSL venv leandojo-v2) - LeanDojo-v2 : DynamicDatabase + serveur RPC Pantograph (See #18430)
├── Lean-11-TorchLean.ipynb # Lean4 kernel - NN verification
├── Lean-11b-TorchLean-Python.ipynb # Python kernel - Implémentation algorithmes
├── Lean-12-Sensitivity-Theorem.ipynb # Python kernel - théorème de sensibilité (Huang 2019, hypercube, signing matrix)
├── Lean-12b-Lean-Sensitivity-Theorem.ipynb # Lean4 (WSL) kernel - companion natif du théorème de sensibilité (preuve 0-sorry du lake sensitivity_lean)
├── Lean-12c-Tensor-Product-Representations-Lean.ipynb # Lean4 (WSL) kernel - algèbre TPR : binding, unbinding, constituent surgery (jumeau empirique SL-13 SymbolicLearning)
├── Lean-15-Grothendieck-Tribute.ipynb # Python kernel - hommage Grothendieck (langage grothendieckien Mathlib)
├── Lean-15b-Lean-Grothendieck.ipynb # Python kernel - atelier pratique Grothendieck (compagnon grothendieck_lean)
├── Lean-15c-Lean-Grothendieck-Companion.ipynb # Lean4 (WSL) kernel - companion formel natif grothendieck_lean (51 modules par leurs énoncés, Epic #11703)
├── Lean-15d-Lean-Grothendieck-Visuel-Python.ipynb # Python kernel - visite guidée visuelle du corpus Grothendieck (7 figures, 3 exercices, sans lake)
├── Lean-16a-Conway-Man-and-Work.ipynb # Python kernel - hommage Conway (l'homme et l'œuvre, noix exécutées depuis conway_lean)
├── Lean-16b-Conway-Game-of-Life-Lean.ipynb # Python kernel - hommage Conway (Game of Life as Computation)
├── Lean-16c-Conway-Game-of-Life-Golly.ipynb # Python kernel - hommage Conway (Game of Life en images, compagnon Golly)
├── Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb # Lean4 (WSL) kernel - Game of Life natif (grille, B3/S23, decide/native_decide, 0 sorry)
├── Lean-16e-Conway-FRACTRAN-Lean-Native.ipynb # Lean4 (WSL) kernel - FRACTRAN natif (machine universelle de Conway, générateur de premiers)
├── Lean-16g-Conway-Canons.ipynb # Python kernel - barreau 2 de l'échelle des témoins : source périodique (canon de Gosper) mesurée, cherchée, certifiée #eval (#12223)
├── Lean-16h-Conway-PatternTour-Native.ipynb # Lean4 (WSL) kernel - tournée des motifs : PatternTour.lean importé et exécuté in-kernel (Epic #11703)
├── Lean-16i-Translateur-Life.ipynb # Python kernel - synthèse d'un translateur minuscule (SAT borné, Loi II, Chantier 2 #12205)
├── Lean-16j-Conway-Hashlife-Correctness-Native.ipynb # Lean4 (WSL) kernel - compagnon Hashlife correctness (cône, MacroCell, 4 murs, marge, batterie adverse, Epic #11703)
├── Lean-13-Kochen-Specker.ipynb # Lean4 kernel - théorème de Kochen-Specker (Pilier 1.B)
├── Lean-13b-CHSH-Tsirelson-Native.ipynb # Lean4 (WSL, conway-build) kernel - borne de Tsirelson : signature, axiomes, frontière classique (Epic #13106)
├── Lean-13c-CHSH-Landau-Saturation.ipynb # Lean4 (WSL) kernel - saturation de Tsirelson : témoin de Pauli, égalité centrale 2√2, forme spectrale (Epic #13106)
├── Lean-13d-CHSH-Indeterminisme-Native.ipynb # Lean4 (WSL) kernel - pont CHSH <-> libre arbitre : modèle local déterministe, frontière état par état, conclusion d'indéterminisme (Epic #13106)
├── Lean-14-Finiteness-Derivatives.ipynb # Python kernel - dérivées symboliques de Brzozowski (finitude, matching linéaire)
├── Lean-14b-Finiteness-Lean-Companion.ipynb # Lean kernel - companion natif du lake finiteness_lean (7 déclarations citées)
├── Lean-16f-Conway-Free-Will-Theorem.ipynb # Python kernel - hommage Conway (théorème du libre arbitre, adossé à FreeWillTheorem.lean)
├── Lean-17a-Knots-Conway-Proofs.ipynb # Python kernel - Conway, les nœuds et la preuve de Piccirillo (noeud de Conway)
├── Lean-17b-Knots-Invariants-Companion.ipynb # Python kernel - invariants de nœuds (PD-codes, Reidemeister, Fox tricolorability), compagnon knot_lean
├── Lean-17c-Knots-Companion-Formel.ipynb # Python kernel - companion formel knot_lean (modules non cités par 17b, murs R2/R3, miroir i18n)
├── Lean-20-Capstone-Digestions-Tao-Python.ipynb # Python kernel - escalier capstone vers la sous-série ANALYSE : digestion du travail formel de T. Tao, règle de chaîne, distance de Ruzsa
├── Lean-21-MIMO-Detection-Flips.ipynb # Python kernel - détection MIMO par flips (seuil 2·log N, companion mimo_lean)
├── Lean-21b-MIMO-Converse-Native.ipynb # Lean4 (WSL) kernel - converse MIMO natif (NormTails, Hanson-Wright, #print axioms)
├── Lean-21c-Descente-Budget.ipynb # Python kernel - budget de descente (décroissance borne les flips, #12219)
├── Lean-22-Galois-Probleme-Inverse-M23.ipynb # Python kernel - problème inverse de Galois (M₂₃ simple prouvé, f₁ degré 23 vérifié)
├── Lean-23-ERC20-Invariant-Companion.ipynb # Python kernel - invariant ERC-20 (lecture statique du lake erc20_lean, Monte-Carlo)
├── Lean-23b-Lean-ERC20-Native-Companion.ipynb # Lean4 (WSL) kernel - ERC-20 natif (17 déclarations résolues par le kernel)
├── Lean-24-Calibration-Native-Companion.ipynb # Lean4 (WSL) kernel - calibration_lean natif (cibles prover P1-P5, #print axioms)
├── Lean-25-Coherence-et-Temoin.ipynb # Python kernel - cohérence de de Finetti (Dutch book, miroir exact de decision_theory_lean)
├── Lean-26-Munkres-Tribute.ipynb # Lean4 (WSL) kernel - hommage Munkres, cours 18.901 dans Mathlib (mathlib_examples, #check/#print axioms natifs)
├── Lean-27-EdgeColoring-Tutte-Companion.ipynb # Lean4 (WSL) kernel - coloration d'arêtes & Tutte (définitions SimpleGraph, Petersen exécutable, decide/eval)
├── Lean-28-Complex-Structure-S6.ipynb # Python kernel - problème de Hopf sur S⁶ (digestion Engel + reproduction plby/HopfProblem piné, comparator double kernel)
├── Lean-29-Hecke-Operators-Native.ipynb # Lean4 (WSL) kernel - opérateurs de Hecke T_p/U_p natifs (lake hecke_lean, #check/#print axioms in-kernel)
├── Lean-30-FormalGroups-Native.ipynb # Lean4 (WSL) kernel - groupes formels multivariés natifs (lake formal_groups_lean, modules Basic/Hom/Additive/Iterates)
├── Lean-31-Euler-Navier-Stokes.ipynb # Python kernel - reproduction pinée Euler/Navier–Stokes, double noyau, confinement, re-dérivation fail-closed, chronologie sourcée de la course Navier–Stokes et GIFs animés de l'écoulement
├── Lean-33-Distribution-Spaces.ipynb # Lean4 (WSL) kernel - espaces de Schwartz natifs (lake calibration_lean, module Calibration.Distribution)
├── Lean-34-Calculabilite-et-Limites.ipynb # Python kernel - Tranche E Epic #15066 : arrêt, point fixe, Gödel I/II, Rosser, Tarski, Löb (lake formal_logic_lean CONSUMER_PINNÉ)
├── Lean-34b-FairBot-Loeb.ipynb # Python kernel - FairBot par Löb (Barasz et al. 2014) : Löb postulé en L2, théorème en L3 (FormalLogic.FairBotLoeb), cadres de Kripke, combat modal GL
├── Lean-24b-Confiance-Preuves-Native.ipynb # Lean4 (WSL) kernel - fiabilité d'un certificat : mis-définition, axiomes de secours (#print axioms), certificat vs headline (lake mathlib_examples)
├── Lean-36-Structures-Finies-MUH-Lean.ipynb # Lean4 (WSL) kernel - Annexe A de Tegmark : structures finies, encodage/complexité, C₃/C₂/NAND, Aut(S), frontière du décideur exhibée (lake tegmark_muh_lean, sans Mathlib)
├── Lean-37-Capstone-Serre100.ipynb # Python kernel - escalier capstone vers la sous-série Serre 100 : entrée, démos, prérequis de la série distillations
├── _run_lean_snippet.sh # Helper WSL : run Lean snippet avec cache Mathlib
├── lean_runner.py # Module Python multi-backend
├── README.md
├── .env.example
├── ANALYSE/ # Sous-série des formalisations d'analyse (Sendov, Tao Analysis I, PFR ×2 — gradation #17545) : [README](ANALYSE/README.md)
│ ├── ANALYSE-01-Sendov-Lean-Python.ipynb # Conjecture de Sendov : énoncé, cas numériques, contexte de la preuve 2026
│ ├── ANALYSE-02-Tao-Lean-Python.ipynb # Analysis I de Tao en lac Lean 4 (teorth/analysis) : architecture, lemmes emblématiques
│ ├── ANALYSE-03-PFR-Lean.ipynb # Conjecture PFR (teorth/pfr) : méthode entropique, cosets F₂³, #check réels
│ ├── ANALYSE-04-PFR-Primitives-Python.ipynb # Les trois primitives de PFR et l'endroit où elles cessent de valoir (#12214)
│ └── README.md
├── Langlands/ # Sous-série formes modulaires et ponts (EPIC #17969) : [README](Langlands/README.md)
│ ├── 01-formes-modulaires-sl2z-hecke.ipynb
│ ├── 02-monstrous-moonshine-invariant-j.ipynb
│ └── README.md
├── Serre100/ # Sous-série distillations du centenaire Serre (EPIC #16334) : [README](Serre100/README.md)
│ ├── 01-corps-finis-borne-hasse.ipynb
│ ├── 02-valeurs-zeta-multiples-finies.ipynb
│ ├── 03-cohomologie-cech-espaces-finis.ipynb
│ ├── 04-lemme-yoneda-categories-finies.ipynb
│ ├── 05-table-de-caracteres.ipynb
│ ├── 06-bulles-minkowski.ipynb
│ ├── 07-zeros-fonctions-l-gaps-gue.ipynb
│ ├── 08-serre-dans-mathlib-Lean.ipynb
│ ├── 09-congruences-tau-lacunarite-delta.ipynb
│ ├── serre100_lean/ # Lake Serre 100 (Hasse, MZV, Yoneda, caractères — modules FR + jumeaux _en)
│ └── README.md
├── assets/ # Images des README de la série ([MANIFEST](assets/readme/MANIFEST.md))
├── scripts/ # Helpers de maintenance de la série ([README](scripts/README.md), _archive/)
├── sensitivity_lean/ # Théorème de sensibilité (Huang 2019, companion Lean-12/12b) - 0 sorry 0 axiome, Lake build natif (jonction Mathlib)
├── finiteness_lean/ # Finitude des dérivées de Brzozowski (companion Lean-14) - 0 sorry, Lake build
├── conway_lean/ # Conway tribute workspace (0 sorry, Lake build)
├── grothendieck_lean/ # Grothendieck tribute workspace (0 sorry, Lake build)
├── knot_lean/ # Knot theory workspace (théorie des nœuds, companion Lean-17a/b, sorries résiduels documentés, Lake build)
├── calibration_lean/ # Cibles de calibration du prouveur multi-agents (Epic #1453, P1-P5) - 0 sorry, Lake build
├── galois_lean/ # Problème inverse de Galois : M₂₃ (Mathieu 23) groupe simple + preuve formelle vendored (Apache-2.0, [KitaKen1/finite-simple-groups-lean](https://github.com/KitaKen1/finite-simple-groups-lean)) - 0 sorry, Lake build ; companion du notebook Lean-22 (Epic #10478, arXiv:2608.08538, août 2026)
├── hecke_lean/ # Opérateurs de Hecke T_p/U_p (port pédagogique de anthropics/fermats-last-theorem, Apache-2.0, toolchain pinée v4.33.0) - 0 sorry, Lake build ; companion du notebook Lean-29
├── formal_groups_lean/ # Groupes formels multivariés (port de anthropics/fermats-last-theorem, Apache-2.0) - 0 sorry, Lake build ; companion du notebook Lean-30
├── formal_logic_lean/ # Logique formelle : Foundation piné + ProvabilityLogic (CONSUMER_PINNÉ) - 0 sorry, Lake build ; companion des notebooks Lean-3b/34/34b (Epic #15066)
├── mimo_lean/ # Détection MIMO et borne converse Hanson-Wright (brique SLT empruntée à YuanheZ/lean-stat-learning-theory) - 0 sorry, Lake build ; companion du notebook Lean-21b
├── tegmark_muh_lean/ # Annexe A de Tegmark 2007 (arXiv:0704.0646) : structures finies, encodage, C₃/C₂/NAND, Aut(S), squelette décideur déclaré - **sans dépendance Mathlib**, 0 sorry, Lake build ; companion du notebook Lean-36
├── mathlib_examples/ # Smoke test Mathlib (ring/linarith/omega/rw, 4 buts) - 0 sorry, Lake build
├── agent_tests/ # Prover daemon (autonomous Lean proof)
│ ├── multi_agent_proof.py # CLI principal
│ ├── lean_server.py # Serveur Lean LSP
│ └── prover/ # Package prover (Microsoft Agent Framework)
│ ├── __init__.py # Exports: MultiAgentSorryProver, AutonomousProver
│ ├── provers.py # Multi-agent + Autonomous prover classes
│ ├── workflow.py # WorkflowBuilder graph (4 agents)
│ ├── agents.py # Agent factory (Search/Tactic/Critic/Coordinator)
│ ├── tools.py # Per-agent tools (file ops, compile, tactics)
│ ├── state.py # ProofState, SorryContext
│ ├── config.py # Providers (z.ai GLM-5.1, local Qwen), demos
│ ├── instructions.py # Agent system prompts
│ ├── lean_utils.py # Sorry extraction, goal state, verification
│ ├── trace.py # Conversation trace logger
│ └── vérifier.py # Lean verification backend
├── examples/
│ ├── basic_logic.lean
│ ├── quantifiers.lean
│ ├── tactics_demo.lean
│ ├── mathlib_examples.lean
│ └── llm_assisted_proof.lean
└── tests/
├── test_leandojo_basic.py # Tests rapides (sans tracing)
├── test_leandojo_repos.py # Tests complets sur repos
└── test_wsl_lean4_jupyter.py # Tests backend WSLProver daemon
Le package agent_tests/prover/ implémente un prouveur autonome Lean 4 utilisant le Microsoft Agent Framework.
Architecture
4 agents spécialisés dans un workflow conditionnel :
- SearchAgent : analyse le contexte, détecte les sorry, identifie les helpers
- TacticAgent : génère des tactiques de preuve (avec outils de compilation)
- VerifyExecutor : vérifie les tactiques via
lake build(non-LLM) - CriticAgent : analyse les erreurs et route vers le bon agent
Usage
# Prouver un sorry dans un fichier .lean
python agent_tests/multi_agent_proof.py --lean path/to/File.lean --sorry-line 128
# Mode autonome (1 agent avec tous les outils)
python agent_tests/multi_agent_proof.py --lean path/to/File.lean --mode autonomous
# Mode multi-agent (4 agents spécialisés)
python agent_tests/multi_agent_proof.py --lean path/to/File.lean --mode multi
# Batch sur des demos
python agent_tests/multi_agent_proof.py --batch --demos 1,2,3Configuration
Le fichier .env dans agent_tests/ ou le répertoire parent configure : - ZAI_API_KEY : clé API z.ai pour GLM-5.1 (raisonnement) - ZAI_BASE_URL : endpoint API z.ai - LEAN_PROJECT_DIR : répertoire du projet Lean (pour lake build)
Connections cross-séries
Les concepts de vérification formelle et de preuve assistée par LLM présentés dans cette série se retrouvent dans d’autres séries du curriculum :
Lean et Théorie des Jeux (GameTheory)
Les notebooks GameTheory side tracks (16b-16f) formalisent en Lean 4 des résultats fondamentaux de théorie des jeux et de choix social :
| résultat | Fichier Lean | Notebook GameTheory | Statut |
|---|---|---|---|
| théorème d’Arrow (impossibilité) | game_theory_lean/SocialChoice/Arrow.lean |
16d | 0 sorry (Geanakoplos 2005) |
| théorème de Sen (libéralisme) | game_theory_lean/SocialChoice/Sen.lean |
16e | 0 sorry (bidirectionnel) |
| Valeur de Shapley | game_theory_lean/CooperativeGames/Shapley.lean |
16b | 0 sorry (caractérisation + unicité ; Banzhaf #4011/#4037/#4130 ; lake cooperative_games_lean/ supprimé post-#4365, contenu absorbé) |
| Modèles de vote (Banks, STV) | game_theory_lean/SocialChoice/Voting.lean |
16f | 0 sorry |
| Gale-Shapley (stable marriage) | game_theory_lean/StableMarriage/GaleShapley.lean |
(pas de notebook dédié) | 0 sorry. gale_shapley_stable, gale_shapley_man_optimal (via exists_isManOptimal, Lattice.lean) et gale_shapley_woman_pessimal prouvés. |
Le notebook Lean-5 (tactiques) et Lean-6 (Mathlib) sont des prérequis directs pour les side tracks Lean de GameTheory.
Lean et SmartContracts
La vérification formelle en Lean (type theory, Curry-Howard) est conceptuellement liée à la vérification formelle des smart contracts :
- SC-14 Formal Verification : Certora/SMTChecker vs. Lean – la même idée de preuve mathématique de correction, mais sur des cibles différentes (Solidity vs. mathématiques). Les méthodes différent : SMT solving (automatique, borné) vs. tactiques interactives (expressif, guidable).
- SC-11 LLM-Assisted Contracts : Le même paradigme d’assistance LLM que les notebooks Lean-7/8/9, appliqué à la génération de smart contracts au lieu de preuves.
- SC-17 E2E Vérifiable Voting : Les résultats de
Voting.lean(théorème du median voter, propriétés Banks/STV) éclairent les propriétés théoriques des systèmes de vote vérifiable.
Lean et Théorie des Nœuds
Le notebook Lean-17b (Invariants de Nœuds) est le pendant pédagogique du projet formel knot_lean/ : les invariants introduits en cours (PD-codes, mouvements de Reidemeister, tricolorabilité de Fox) y sont portés en Lean 4, avec un accent sur le théorème de transfert – la tricolorabilité est préservée par un twist R1 connecté (Epic #2874).
| résultat | Fichier Lean | Notebook | Statut |
|---|---|---|---|
| Transfert forward (R1 connecté préserve la tricolorabilité) | knot_lean/Knots/Invariant.lean |
17b | 0 sorry (#3000, sorry-free) |
| Transfert backward (partiel) | knot_lean/Knots/Invariant.lean |
17b | Path B shipped (#3003/#4035) : invariant de Fox classique restauré (arc-égalité c₂=c₄) + pont GF(3) triColorFoxCondition_iff_sum_mod_three prouvé ; num prouvé #3163 ; 2 résiduels §9.1 (fox/col all-distinct) OPEN research-HOLD (BG-prover #2874) |
| Tricolorabilité du noeud de Conway (11n34) | knot_lean/Knots/Conway.lean |
17a | scaffolding |
| Théorème d’invariance par Reidemeister (PL topology) | knot_lean/Knots/Reidemeister.lean |
17b | 2 sorry (out-of-scope PL) |
Le notebook Lean-17a donne le contexte historique (noeud de Conway, slice-genre, preuve de Piccirillo 2020) qui motive le formalisme. Voir LEAN_INVENTORY.md pour l’état détaillé par module.
Lecture transversale
La mer qui monte : une grille de lecture grothendieckienne du dépôt (changement de représentation, certification A/B/C).
FAQ
Le kernel lean4-wsl ne démarre pas (timeout après 60s)
Cause : le wrapper Python (~/.lean4-kernel-wrapper.py) ne trouve pas le venv Lean ou le REPL. vérifier :
# Dans WSL
test -f ~/.lean4-venv/bin/python3 && echo "venv OK" || echo "venv MISSING"
test -f ~/.elan/bin/repl && echo "repl OK" || echo "repl MISSING"
test -d ~/lean-projects/notebook_context && echo "context OK" || echo "context MISSING"Si un élément manque, relancer le setup : bash MyIA.AI.Notebooks/GameTheory/scripts/setup_wsl_lean4.sh. Si le kernel.json pointe vers l’ancien wrapper bash (~/lean4-jupyter-wrapper.sh), le mettre à jour pour pointer vers ~/.lean4-kernel-wrapper.py (incident 2026-05-27).
lake build échoue avec des erreurs Mathlib inattendues
Cause fréquente : la toolchain Lean locale est désynchronisée du lean-toolchain du projet. Lean 4 évolue rapidement et Mathlib suit.
# vérifier la toolchain requise par le projet
cat lean-toolchain # ex: leanprover/lean4:v4.x.0
# vérifier la toolchain installée
elan show
# Forcer la réinstallation de la bonne version
elan toolchain install leanprover/lean4:v4.x.0
lake exe cache get # Télécharger les artifacts Mathlib précompilés
lake build # Doit passerComment lire les erreurs type mismatch ?
Lean 4 signale type mismatch quand le type attendu et le type fourni ne coïncident pas. Les causes les plus fréquentes :
- Universe level :
Type uvsType— ajouteruniverse uou utiliserSort _. - Implicit arguments : Lean ne peut pas inférer un argument implicite. Essayer
@nom_fonctionpour rendre tous les arguments explicites. - Definitional equality :
NatvsInt,ListvsArray— utiliser les conversions explicites (Int.ofNat,List.toArray). - Motive mismatch dans
induction/cases: le motif (motive) ne généralise pas correctement. Essayergeneralizing hou restructurer le but avechaveavant l’induction.
sorry dans un notebook pédagogique, c’est grave ?
Non dans les cellules d’exercice (stub pour l’étudiant). Oui dans le code de production (preuves formelles). La convention CoursIA :
- Cellules d’exercice :
sorry= placeholder étudiant, normal et attendu. - Preuves certifiées (ex:
conway_lean/,grothendieck_lean/,game_theory_lean/) :sorry= axiome implicite = trou dans la chaîne de certification. Le compteurgrep -c sorryest suivi par les agents du dépôt.
Voir LEAN_INVENTORY.md pour l’état détaillé des preuves par module.
Quelle est la différence entre Lean-17a et Lean-17b ?
Les deux notebooks couvrent la théorie des nœuds sous des angles complémentaires :
- Lean-17a (Conway, les nœuds et la preuve de Piccirillo) : hommage narratif. Le contexte mathématique et historique – le noeud de Conway (11n34), le slice-genre, le nombre de dénouement, et la preuve de Piccirillo (2020) que le noeud de Conway n’est pas slice. Aucun exercice : c’est une lecture.
- Lean-17b (Invariants de Nœuds) : atelier pratique et companion du projet formel
knot_lean/. On y manipule les PD-codes, les mouvements de Reidemeister et la tricolorabilité de Fox, avec des exercices de calcul et de vérification d’invariants.
Lean-17a donne le pourquoi (motivation historique) ; Lean-17b donne le comment (calcul des invariants, port formel).
Conclusion / Prochaines étapes
Ce que vous avez appris
Lean n’est pas un langage de programmation de plus : c’est le point où le code devient une preuve. En parcourant cette série, vous avez traversé le spectre de la vérification formelle :
- Les fondations (Lean-1 Setup à Lean-6) : installer l’outil, manipuler les types dépendants, comprendre l’isomorphisme de Curry-Howard — un programme est une preuve, un type est une proposition.
- Prouver en pratique (Lean-7 à Lean-12) : tactiques, lemmes, induction, l’art de réduire un énoncé jusqu’à ce que
rfloudecidele closent. Vous avez vu qu’une preuve formelle n’est pas une invention — c’est un dialogue avec un vérificateur qui n’accepte rien sur confiance. - Les mathématiques vivantes (Lean-15 à Lean-17b) : Game of Life (Hashlife), théorie des jeux sociaux (Arrow, Sen, Shapley), topologie (Grothendieck), théorie des nœuds (Piccirillo, tricolorabilité de Fox). Chaque domaine porté en Lean devient une certification — le
sorryrésiduel y est tracé comme une dette, pas caché.
Prochaines étapes
- Poussez un port jusqu’au bout : le projet
knot_lean/est le companion formel de Lean-17b. Les invariants de nœuds (PD-codes, Reidemeister, Fox) y sont portés avec quelquessorryrésiduels documentés — un terrain concret où une preuve formelle est en cours, pas achevée. - Croisez avec la théorie des jeux : les résultats formels d’Arrow/Sen/Shapley/Voting (notebooks 16b-16f) rencontrent la série GameTheory — où le choix social est étudié à la fois formellement et computationnellement.
- Appliquez au monde réel : la vérification formelle n’est pas qu’abstraite. La série SmartContracts (SC-14) applique les mêmes principes aux smart contracts — SMT solvers automatiques bornés d’un côté, Lean interactif expressif de l’autre, même ambition : certifier la correction d’un programme exécuté.
- Élargissez au Web Sémantique : les shapes SHACL sont des invariants sur les données, analogues aux spécifications Lean. La série SemanticWeb (SW-7 OWL, SW-8 SHACL) explore une autre face de la certification — valider la cohérence d’une base de connaissances plutôt que prouver un théorème.
- Relisez la série sous l’angle de la certification : la Lecture transversale relie ce geste — certifier par changement de représentation — à l’ensemble du dépôt CoursIA.
Le fil rouge
Le titre annonce un solveur mathématique et de la vérification formelle. Mais le geste que cette série enseigne est plus profond : ne rien laisser sur confiance. Un theorem en Lean n’est pas une affirmation, c’est un objet vérifié mécaniquement ; un sorry n’est pas un raccourci, c’est un trou dans la chaîne de certification que l’on trace explicitement. Les domaines changent (topologie, choix social, nœuds, cellular automata), les tactiques changent (induction, native_decide, aesop), mais l’exigence reste — prouver, pas supposer. C’est elle que vous emportez au-delà de cette série.
Licence
Voir la licence du repository principal.
Comment installer Lean 4 sous Windows ?
Lean 4 ne tourne pas nativement sous Windows pour les notebooks. La configuration recommandée utilise WSL 2 (Ubuntu) :
wsl --install -d Ubuntu(si pas encore fait)curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | shelan default leanprover/lean4:stablescripts/setup_wsl_lean4.sh(crée le venv, le wrapper, et enregistre le kernel)Le notebook Lean-01-Setup-Lean-Python guide l’installation complète et vérifie chaque composant.