Skip to content

build(mimo,#14773): migrate lake to Lean 4.33 #15964

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Sep 13, 2026
Merged

build(mimo,#14773): migrate lake to Lean 4.33 #15964

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 13 additions & 7 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
# mimo_lean — Détection MIMO par descente à flips (Lean 4)

Port formel de l'algorithme de détection MIMO par flips de coordonnées
(Papailiopoulos, 2026 — issue #10984). Le lake naît directement sur
`v4.32.1` (Mathlib résolu à `520045ab14e26149ee970e2e617ca04b09bde5d6`,
fin de la migration #10986) et suit la convention i18n #4980
(Papailiopoulos, 2026 — issue #10984). Le lake cible désormais
`v4.33.0` (Mathlib résolu à `db584cd6d46c92f209a44c0f1c829460d327499d`,
rollout #14773) et suit la convention i18n #4980
(docstrings FR par défaut, sibling `_en` avec namespace `Mimo_en`).

## Phases et libs compilées
Expand Down Expand Up @@ -40,12 +40,18 @@ autres lakes du dépôt).

| Lake | Source | Pin | Consommé par |
|----------------|-------------------------------------------------------------------------|-------------------------------------------|------------------------------------|
| **mathlib4** | github.com/leanprover-community/mathlib4.git | `v4.32.1` (résolu `520045ab…`) | Objective, Lmmse, Converse, Bridge, NormTails |
| **slt** | github.com/YuanheZ/lean-stat-learning-theory.git (Apache 2.0) | `d0f506f0a695018265dccb33bcb05e2f5ca1c876` | Converse (Hanson–Wright), NormTails (Lipschitz) |
| **mathlib4** | github.com/leanprover-community/mathlib4.git | `v4.33.0` (résolu `db584cd6…`) | Objective, Lmmse, Converse, Bridge, NormTails |
| **slt** | github.com/jsboige/lean-stat-learning-theory.git (fork Apache 2.0) | `0b1020a4771037b89d0b3809913608d177c09a14` | Converse (Hanson–Wright), NormTails (Lipschitz) |

Le pin SLT est **identique** à `lake-manifest.json` — la `require` ne dérive
pas. Aucune mise à jour de SLT n'est prévue sans revue dédiée (sécurité de
la frontière formelle).
pas. Il ajoute à la base upstream `d0f506f0a695018265dccb33bcb05e2f5ca1c876`
une seule adaptation : la preuve explicite de non-négativité du cas de rayon
nul dans `SLT.HansonWright`, nécessaire sous Lean 4.33. Le lake SLT cible encore
Lean/Mathlib 4.32 ; dans `lakefile.lean`, Mathlib est donc déclaré en dernier afin
que Lake 5 sélectionne sa fermeture transitive 4.33 (Batteries, Qq, Cli, etc.)
plutôt que celle héritée de SLT. Cet ordre est une contrainte de résolution
documentée, pas un tri cosmétique. Toute autre mise à jour de SLT demande une
revue dédiée (sécurité de la frontière formelle).

## Inventaire détaillé des phases

Expand Down
34 changes: 17 additions & 17 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,31 +1,31 @@
{"version": "1.2.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/YuanheZ/lean-stat-learning-theory.git",
[{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "d0f506f0a695018265dccb33bcb05e2f5ca1c876",
"name": "slt",
"rev": "db584cd6d46c92f209a44c0f1c829460d327499d",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "d0f506f0a695018265dccb33bcb05e2f5ca1c876",
"inputRev": "db584cd6d46c92f209a44c0f1c829460d327499d",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
{"url": "https://github.com/jsboige/lean-stat-learning-theory.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "520045ab14e26149ee970e2e617ca04b09bde5d6",
"name": "mathlib",
"rev": "0b1020a4771037b89d0b3809913608d177c09a14",
"name": "slt",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.32.1",
"inputRev": "0b1020a4771037b89d0b3809913608d177c09a14",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
"rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -35,7 +35,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
"rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
"name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -45,7 +45,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
"rev": "16f02aa7642864af59f1ff0e384a015994db9118",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -55,7 +55,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
"rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -65,7 +65,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
"rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -75,7 +75,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
"rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
Expand All @@ -85,7 +85,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
"rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -95,10 +95,10 @@
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
"rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.32.0",
"inputRev": "v4.33.0",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "mimo_lean",
Expand Down
26 changes: 17 additions & 9 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ open Lake DSL
# Lake mimo_lean — détection MIMO par descente à flips (Lean 4)

Port formel de l'algorithme de détection MIMO par flips de coordonnées
(Papailiopoulos, 2026 — cf issue #10984). Le lake naît directement sur
`v4.32.1` (fin de la migration #10986) — Mathlib résolu à
`520045ab14e26149ee970e2e617ca04b09bde5d6` (cf `lake-manifest.json`).
(Papailiopoulos, 2026 — cf issue #10984). Le lake cible désormais
`v4.33.0` (rollout #14773) — Mathlib résolu à
`db584cd6d46c92f209a44c0f1c829460d327499d` (cf `lake-manifest.json`).

Six libs compilées, deux phases utilitaires + quatre phases du papier §11 :

Expand All @@ -25,8 +25,9 @@ Six libs compilées, deux phases utilitaires + quatre phases du papier §11 :
- **Phase 3b / Converse** (`Converse.lean`) : converse §11 — concentration
Hanson–Wright du bruit (`‖w‖²` chi-square), union bound
`(1−p)^n ≤ e^{−np}`, appui sur le lake externe
`YuanheZ/lean-stat-learning-theory` (SLT, pinned
`d0f506f0a695018265dccb33bcb05e2f5ca1c876`, Apache 2.0).
`YuanheZ/lean-stat-learning-theory` (SLT, base
`d0f506f0a695018265dccb33bcb05e2f5ca1c876`, Apache 2.0) avec un commit de
compatibilité Lean 4.33 borné à la preuve du cas de rayon nul.
- **Phase 4 / Bridge** (`Bridge.lean`, grignotage #11148) : pont entre
`mimoObj` (Phase 2) et converse (Phase 3b) — identité de différence de
coût `cost_diff`, fragment de converse connecté au ML.
Expand All @@ -41,11 +42,18 @@ Convention i18n #4980 : docstrings FR par défaut, sibling `_en`
package «mimo_lean» where
leanOptions := #[⟨`autoImplicit, false⟩]

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "v4.32.1"

/-
Le fork SLT ajoute à la base upstream d0f506f une unique adaptation de preuve
pour Lean 4.33 ; son lake reste épinglé à Mathlib 4.32. Lake 5 résout les
dépendances directes dans l'ordre inverse de leur déclaration : Mathlib doit
rester en dernier pour que sa fermeture transitive 4.33 (Batteries, Qq, Cli,
etc.) l'emporte sur celle de SLT.
-/
require slt from git
"https://github.com/YuanheZ/lean-stat-learning-theory.git" @ "d0f506f0a695018265dccb33bcb05e2f5ca1c876"
"https://github.com/jsboige/lean-stat-learning-theory.git" @ "0b1020a4771037b89d0b3809913608d177c09a14"

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "db584cd6d46c92f209a44c0f1c829460d327499d"

@[default_target]
lean_lib «Descent» where
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lean-toolchain
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.32.1
leanprover/lean4:v4.33.0
Loading