Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 2 additions & 0 deletions MyIA.AI.Notebooks/GameTheory/social_choice_lean/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,8 @@ Résultats formalisés par Peters :
3. **Phase 3** : Portage sélectif dans notre framework `PrefOrder` (impossibilités Condorcet, règles de scoring)

**Différences de framework** :


| Aspect | Notre projet (ChaseNorman) | DominikPeters |
|--------|---------------------------|---------------|
| Type de préférence | `PrefOrder α` (réflexif, total, transitif) | `LinearOrder A` (strict, Mathlib) |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -444,8 +444,8 @@
"Reprenons le système vedette de la serie : le **tri auto-organise** vue-cellule\n",
"d'[ICT-2](ICT-2-SelfSortingMorphogenesis.ipynb) (tableaux chimeriques alternant\n",
"les algotypes `bubble`/`insertion`). On en extrait une signature naturelle : le\n",
"**deplacement net** de chaque cellule, $|{\\rm position\\ initiale} - {\\rm position\\\n",
"finale}|$, sur de nombreuses permutations aleatoires. Certaines cellules voyagent\n",
"**deplacement net** de chaque cellule, $\\lvert {\\rm position\\ initiale} - {\\rm position\\\n",
"finale} \\rvert$, sur de nombreuses permutations aleatoires. Certaines cellules voyagent\n",
"loin, d'autres a peine : la distribution a une queue. Est-elle scale-free ?"
]
},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2433,7 +2433,7 @@
"\n",
"### Problemes etudies\n",
"\n",
"| Problème | Taille $|S|$ | Cout | Difficulte principale |\n",
"| Problème | Taille $\\lvert S\\rvert$ | Cout | Difficulte principale |\n",
"|----------|-------------|------|-----------------------|\n",
"| Aspirateur | 8 | Uniforme | Trivial, sert de modèle pedagogique |\n",
"| 8-Puzzle | 181 440 | Uniforme | Taille de l'espace, profondeur des solutions |\n",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -703,7 +703,7 @@
"|---------|-------------------|\n",
"| Fonction objectif | délégué `Func<double[], double>` (Sphere, Ackley) |\n",
"| Voisinage | perturbation gaussienne (Box-Muller), bornée au domaine |\n",
"| Critère de Metropolis | `delta <= 0 || rng.NextDouble() < Math.Exp(-delta / T)` |\n",
"| Critère de Metropolis | `delta <= 0 \\|\\| rng.NextDouble() < Math.Exp(-delta / T)` |\n",
"| Refroidissement | géométrique `T *= alpha` |\n",
"| Reproductibilité | `Random(42)` (seed fixe hors des fonctions) |\n",
"\n",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,6 @@
" The below script needs to be able to find the current output cell; this is an easy method to get it.\r\n",
" </div>\r\n",
" <script type='text/javascript'>\r\n",

" function timeout(ms, promise) {\r\n",
" return new Promise(function (resolve, reject) {\r\n",
" setTimeout(function () {\r\n",
Expand All @@ -108,10 +107,7 @@
" })\r\n",
" }\r\n",
"\r\n",


"\r\n",

"\r\n",
" if (!rootUrl.endsWith('/')) {\r\n",
" rootUrl = `${rootUrl}/`;\r\n",
Expand All @@ -126,7 +122,6 @@
" headers: {\r\n",
" 'Content-Type': 'text/plain'\r\n",
" },\r\n",

" }));\r\n",
"\r\n",
" if (response.status == 200) {\r\n",
Expand All @@ -138,8 +133,6 @@
" }\r\n",
"}\r\n",
"\r\n",


" .then((root) => {\r\n",
" // use probing to find host url and api resources\r\n",
" // load interactive helpers and language services\r\n",
Expand Down Expand Up @@ -188,13 +181,11 @@
" \r\n",
" \r\n",
" require_script.onload = function() {\r\n",

" };\r\n",
"\r\n",
" document.getElementsByTagName('head')[0].appendChild(require_script);\r\n",
"}\r\n",
"else {\r\n",

"}\r\n",
"\r\n",
" </script>\r\n",
Expand Down Expand Up @@ -1213,7 +1204,7 @@
"| Sous-populations | 2 | Caryotype : [0..15] pour la position, [16..31] pour la vitesse |\n",
"| Stratégie gene 0 | `DefaultMetaHeuristic` | Crossover et mutation actifs sur la position |\n",
"| Stratégie gene 1 | `NoOpMetaHeuristic` | Les parents passent inchanges, seul l'elitisme agit sur la vitesse |\n",
"| Scope | `Crossover | Mutation` | Seuls crossover et mutation passent par les sous-populations |\n",
"| Scope | `Crossover \\| Mutation` | Seuls crossover et mutation passent par les sous-populations |\n",
"| Reinsertion | Globale (par defaut) | L'elitisme s'applique sur les individus reconstruits |\n",
"\n",
"**Points cles** :\n",
Expand Down Expand Up @@ -1661,7 +1652,7 @@
"| **EukaryoteChromosome** | Decoupe un chromosome parent en sous-chromosomes (caryotype) | `GetKaryotype()` decoupe, `UpdateParent()` resync |\n",
"| **SubPopulation** | Population isolee pour une partition du genome | Herite de `MetaPopulation`, contextes separe |\n",
"| **SubPopulationContext** | Contexte d'evolution local a une sous-population | Cache de paramètres indépendant |\n",
"| **EukaryoteMetaHeuristic** | Orchestrateur : applique une sous-heuristique par partition | Scope canonique : `Crossover | Mutation` |\n",
"| **EukaryoteMetaHeuristic** | Orchestrateur : applique une sous-heuristique par partition | Scope canonique : `Crossover \\| Mutation` |\n",
"| **PerformSubOperator** | Recombine les résultats de chaque sous-population | Reconstruit des individus complets |\n",
"\n",
"### Principes de conception\n",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@
"\n",
"| moteur | équations | refroidissement | opérateur bubble-net |\n",
"|---|---|---|---|\n",
"| MGS `WhaleOptimisation` | Mirjalili & Lewis 2016, Eq. (2.3)-(2.5) | a : 2 → 0 linéaire (a2 : −1 → −2 pour l) | spirale `|X*−X|·e^{bl}·cos(2πl) + X*`, b = 1 |\n",
"| MGS `WhaleOptimisation` | Mirjalili & Lewis 2016, Eq. (2.3)-(2.5) | a : 2 → 0 linéaire (a2 : −1 → −2 pour l) | spirale `\\|X*−X\\|·e^{bl}·cos(2πl) + X*`, b = 1 |\n",
"| MGS `WhaleOptimisationNaive` | idem | idem | **combinaison convexe `0,5·X + 0,5·X*`** |\n",
"| mealpy `OriginalWOA` | Mirjalili & Lewis 2016 | a = 2 − 2·epoch/epochs (idem) | spirale canonique |\n",
"\n",
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Search/Part4-Metaheuristics/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ Cette partie se compose de trente-cinq notebooks .NET Interactive (C#), héberg
| 18 | [MGS-18-CecBanc](MGS-18-CecBanc.ipynb) | **Consolidation du banc CEC** — shift+rotate combinés (le protocole standard de dé-biais) | décorateurs composés `RotatedFitness(ShiftedFitness(inner, offset), M)` (Givens orthogonale) ; banc à 4 variantes (plain/shifted/rotated/combined), étend `CenterBiasBenchmark` ; 8 optimiseurs sous shift+rotate sur Ackley+Rosenbrock ; les biais isolés (WOA central MGS-10, GA axe MGS-12) se composent — effet sub-additif ou super-additif selon le paysage | ~50 min |
| 19 | [MGS-19-MetropolisReinsertion](MGS-19-MetropolisReinsertion.ipynb) | **Recuit simulé décomposé** — l'opérateur de Metropolis débranché de SA et greffé seul sur un GA | `MetropolisReinsertion` isolé du compound `SimulatedAnnealing` et injecté via `MetaGeneticAlgorithm.Reinsertion` ; banc 5 configs (pairwise greedy contrôle, 3 températures Metropolis, élitiste référence) sur Sphere/Rastrigin/Ackley + limite frozen ; verdict honnête **négatif** — l'acceptation `exp(Δ/T)` détachée du couplage perturbation+acceptation ne porte pas le bénéfice du recuit | ~45 min |
| 21 | [MGS-21-Representation-vs-Algorithme](MGS-21-Representation-vs-Algorithme.ipynb) | **Représentation × algorithme : le plan croisé Sudoku** — quel facteur pèse le plus ? | deux représentations (R1 vecteur continu + décodage arrondi, R2 grille à permutations de lignes via l'algèbre de swaps) × deux moteurs (PSO composé, GA permutation), budget ~8 000 évaluations, 4 graines {0,1,7,42}, critère de verdict pré-enregistré ; verdict en deux temps — la représentation domine la colonne PSO (−39 conflits vs −34,5/−6 pour l'algorithme), comparable sur la colonne GA ; 4/4 résolutions en R2/GA, aucune en R1 ; cause mesurée : 100 % des candidats R1 décodés tombent hors de l'espace admissible | ~40 min |
| 22 → 31 | [Campagne **MGS vs mealpy**](MGS-vs-mealpy/README.md) — **10 notebooks** (PSO, DE, SA, WOA, EO, FBI, BBPSO, GA, Scatter Search, synthèse) | **Confrontation externe systématique** — la même expérience (protocole apparié Sudoku-Easy[0], budget ~8 000 évals, graines {0,1,7,42}, déterminisme 8/8 ou 12/12), deux bibliothèques (MGS C# .NET 9 vs mealpy 3.0.2 Python/NumPy via PythonNet dans le kernel .NET), un verdict quantitatif. Chaque paire isole un mécanisme (sélection greedy vs réinsertion de population, bruit A1 N(0,1) vs uniforme, écart d'ancrage, ablation de couche mémétique) et tranche sur la question « le moteur ou la stratégie ? » | voir [table des paires](MGS-vs-mealpy/README.md#table-des-paires) |
| 22 → 31 | [Campagne **MGS vs mealpy**](MGS-vs-mealpy/README.md) — **10 notebooks** (PSO, DE, SA, WOA, EO, FBI, BBPSO, GA, Scatter Search, synthèse) | **Confrontation externe systématique** — la même expérience (protocole apparié Sudoku-Easy[0], budget ~8 000 évals, graines {0,1,7,42}, déterminisme 8/8 ou 12/12), deux bibliothèques (MGS C# .NET 9 vs mealpy 3.0.2 Python/NumPy via PythonNet dans le kernel .NET), un verdict quantitatif. Chaque paire isole un mécanisme (sélection greedy vs réinsertion de population, bruit A1 N(0,1) vs uniforme, écart d'ancrage, ablation de couche mémétique) et tranche sur la question « le moteur ou la stratégie ? » | voir [table des paires](MGS-vs-mealpy/README.md#table-des-paires) | |

Les 8 figures MGS-7b (heatmaps de la projection N-D des paysages Sphere/Rastrigin/Schwefel) sont cataloguées dans [`assets/readme/MANIFEST.md`](assets/readme/MANIFEST.md) avec leurs **descriptions visuelles** verbatim (audit vision MiniMax M3 c.755, doctrine #5780) — voir notamment la note disclosed sur la convergence visuelle des heatmaps Rastrigin-d2/d10/d30 en projection MAX (moyennes RGB identiques à 2 décimales près).

Expand Down
2 changes: 2 additions & 0 deletions MyIA.AI.Notebooks/Search/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -148,6 +148,7 @@ Problèmes du monde réel adaptés de projets étudiants. Chaque application est
| 13 | [App-20-SudokuBenchmark-Python](Applications/CSP/App-20-SudokuBenchmark-Python.html) | ~50 min | Benchmark 4 solveurs Sudoku (backtracking naïf → optimisé → contraintes) sur banc Easy/Medium/Hard : dénombrement du travail | Synthèse série |
| 13 (C#) | [App-20b-SudokuBenchmark-CSharp](Applications/CSP/App-20b-SudokuBenchmark-CSharp.html) | ~50 min | Twin C# du 13 : mêmes solveurs from-scratch en .NET, comparaison des écosystèmes | Jumeau .NET |
| 16 | [App-26-CoveringArrays-Guarantee-Audit](Applications/CSP/App-26-CoveringArrays-Guarantee-Audit.ipynb) | ~55 min | Covering Arrays : oracle constraint-aware, set cover CP-SAT exact, bornes et baselines IPOG/AETG-like — distillation PrCon H4 (Valérian Pichot) | Projet étudiant (PrCon PR #58) |

Les autres jumeaux C# de la sous-série CSP (N-Queens, GraphColoring, NurseScheduling, JobShop, Timetabling, Minesweeper, Wordle, MiniZinc, Picross, SportsScheduling) suivent le même principe : ré-implémentation .NET du notebook Python de référence, solveurs from-scratch ou OR-Tools natif selon le sujet (marathon #4956).

### Applications Hybrides / Métaheuristiques (`Applications/Hybrid/`)
Expand All @@ -167,6 +168,7 @@ Les autres jumeaux C# de la sous-série CSP (N-Queens, GraphColoring, NurseSched
| 10 | [App-18b-HyperparameterTuning-CSharp](Applications/Hybrid/App-18b-HyperparameterTuning-CSharp.html) | ~35 min | **Jumeau C#** — tuning GA/PSO from-scratch .NET, parité #4956 | Jumeau .NET |
| 11 | [App-18b-HyperparameterTuning-Python](Applications/Hybrid/App-18b-HyperparameterTuning-Python.html) | ~35 min | **Jumeau Python from-scratch** — GP+EI, GA, PSO numpy + pont Optuna, parité #4956 | Jumeau Python |
| 12 | [App-22-AlgorithmSelection-Python](Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb) | ~45 min | Sélection empirique d'algorithmes : 3 jeux, 13 familles conceptuelles / 14 étiquettes mesurées, non-commensurabilité + Pareto + choix sous préférences — hommage PR IS #42 (Théodore Deguest) | Projet étudiant (IS PR #42) |

---

## Navigation entre sous-séries
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Search/discrepancy_lean/FORMAL_STATUS.md
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ Beck-Fiala and Komlós Bounds Beyond Banaszczyk* (arXiv:2508.03961, 2025).
| p2 (familles aléatoires) | `coinDist` (n-échantillon fairCoin comme `Distribution (Fin n → Bool)`), `familyExpect`/`familyProb` (loi produit coinDist^m sur `Fin m → Fin n → Bool`), `familyExpect_prod_blocks` (**indépendance des blocs** : E[∏_k f k (F k)] = ∏_k E[f k] par `Fintype.prod_sum` — Fubini discret), `familyExpect_add`/`_one`, `familyProb_compl`, et le théorème d'application `family_tail_ge` : ℙ[∃ k, Z_{F k}² ≥ n/2] ≥ 1 − (11/12)^m | brique P2 | **PROUVÉ** (p2, 08-26) | p3 union bound sur les 2^n colorations, p4 contrôle de degree (hoeffding_upper_tail) |
| p1a | Moments de la somme de Rademacher colorée : `expect_rademacherSum_eq_zero` (`E[Z] = 0`), `expect_rademacherSum_sq` (`E[Z²] = ∑ (c i)²`), corollaire coloration (`E[Z²] = n`) + briques `sampleExpect_coord_mul_coord` (factorisation 2-coordonnées, extension kernel), `prod_two_special`, `fairCoin`/`boolSign` | brique P2 | **PROUVÉ** (p1a, 08-25) | uniformité en `c` établie ; p1b = 4ᵉ moment + Paley–Zygmund |
| p3 (union bound) | `colorOf` (encodage booléen → coloration ; `Fin n → ℤ` n'est PAS un Fintype, les colorations sont dénombrées comme IMAGE des `2^n` booléens), `indicator_bUnion_le_sum` (indicatrice d'union ≤ somme d'indicatrices, `Finset.induction_on`), `familyExpect_sum_finset` (linéarité Finset), `familyProb_union_le` (union bound en probabilité via `sampleExpect_mono`), `card_colorings_le` (≤ 2^n par `Finset.card_image_le`), `exists_of_familyProb_pos` (probabilité > 0 ⇒ témoin), et le théorème d'application `exists_family_beats_all_colorings` : pour n ≥ 1 il existe une famille de 12n tirages battant TOUTES les colorations (ℙ[échec] ≤ 2^n·(11/12)^(12n) < 1, numérie par induction `(2·(11/12)^12)^t < 1`) | brique P2 | **PROUVÉ** (p3, 08-26) | le second passage probabiliste (existentiel) est complet ; reste p4 contrôle de degré (`hoeffding_upper_tail`) + assemblage final ErdosSpencerLB |
| p4 (contrôle du degré + assemblage) | `rademacherSum_eq_two_sub` (identité Z = 2·(somme des coords vraies) − somme totale, pont alea signé ↔ sommes d'ensembles), `blockOf`/`drawSet`/`pairFamily` (bloc de t = k/12 points via `Fin.castLEEmb`, tirage → coordonnées vraies, FAMILLE APPARIÉE (drawSet, bloc \\ drawSet)), `blockOf_sum`/`drawSet_sum`/`drawSet_subset`, `drawSet_mem`/`compDraw_mem`, `degree_pairFamily_le` (degré ≤ m par injection vers `Finset.range m` : chaque paire est disjointe donc un point apparaît au plus une fois par tirage), et le THÉORÈME FINAL `erdos_spencer_lb_explicit` : ∀ n k ≥ 1, k ≤ n → ∃ F, maxDegree F ≤ k ∧ ∀ C coloration, Nat.sqrt k ≤ 14 * discrepancy F C — petit k < 12 singletons, gros k = 12 tirages par bloc de k/12 points, triangulaire |Z| ≤ |x| + |x−s| ≤ 2·disc, k ≤ 23t ≤ 184·disc² | brique P2 | **PROUVÉ** (p4, 08-26, axiomes [propext, Classical.choice, Quot.sound]) | **P2 EST ASSEMBLÉ** à constante explicite √k/14 ; la forme optimiste √k/2 (`ErdosSpencerLB`) reste une `Prop` OUVERTE (obstruction structurelle : Paley–Zygmund force m ≥ 12t tirages, degré force m ≤ k — documenté dans le statut du module) |
| p4 (contrôle du degré + assemblage) | `rademacherSum_eq_two_sub` (identité Z = 2·(somme des coords vraies) − somme totale, pont alea signé ↔ sommes d'ensembles), `blockOf`/`drawSet`/`pairFamily` (bloc de t = k/12 points via `Fin.castLEEmb`, tirage → coordonnées vraies, FAMILLE APPARIÉE (drawSet, bloc \\ drawSet)), `blockOf_sum`/`drawSet_sum`/`drawSet_subset`, `drawSet_mem`/`compDraw_mem`, `degree_pairFamily_le` (degré ≤ m par injection vers `Finset.range m` : chaque paire est disjointe donc un point apparaît au plus une fois par tirage), et le THÉORÈME FINAL `erdos_spencer_lb_explicit` : ∀ n k ≥ 1, k ≤ n → ∃ F, maxDegree F ≤ k ∧ ∀ C coloration, Nat.sqrt k ≤ 14 * discrepancy F C — petit k < 12 singletons, gros k = 12 tirages par bloc de k/12 points, triangulaire \|Z\| ≤ \|x\| + \|x−s\| ≤ 2·disc, k ≤ 23t ≤ 184·disc² | brique P2 | **PROUVÉ** (p4, 08-26, axiomes [propext, Classical.choice, Quot.sound]) | **P2 EST ASSEMBLÉ** à constante explicite √k/14 ; la forme optimiste √k/2 (`ErdosSpencerLB`) reste une `Prop` OUVERTE (obstruction structurelle : Paley–Zygmund force m ≥ 12t tirages, degré force m ≤ k — documenté dans le statut du module) |
| P3 | Banaszczyk 1998 / formes fortes des papiers 2025 **et 2026** | aspiration | **NON ENGAGÉ** — exige SDP + dualité, indépendance spectrale affine, brownien discret guidé, concentration matricielle : **aucun de cet étage n'existe dans Mathlib** (vérifié 2026-08-24). **Réaudité 2026-09-13** contre le Mathlib pinné (`520045ab`, v4.32.1) : le contournement proposé par arXiv:2609.11189 ne supprime pas l'obstruction, il la **déplace** — sa route exige la *variation totale directionnelle* d'une densité sur convexe ouvert et la *transformée de Banaszczyk* préservée sous translation, deux notions **absentes du même Mathlib** (`Banaszczyk` : 0 occurrence ; `totalVariation` n'existe que pour les mesures signées ; la théorie BV de Mathlib concerne la dérivabilité a.e. des fonctions de `ℝ`). Ce que ce papier rapproche, ce sont les *socles* : gaussiennes (`Probability/Distributions/Gaussian/*`) et `ConvexBody` (`Analysis/Convex/Body.lean`) sont présents ; le **pont** manque. Documenté, jamais promis. | — |

### Statut épistémique — mise à jour 2026-09-13
Expand Down
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/Sudoku/Sudoku-15-Infer-Csharp.ipynb
Original file line number Diff line number Diff line change
Expand Up @@ -1110,8 +1110,8 @@
"|--------|---------|\n",
"| Première résolution | Compilation initiale du modèle (non mesuré ici, machine-dépendant) |\n",
"| Seconde résolution | Modèle déjà compilé (non mesuré ici, machine-dépendant) |\n",
"| Erreurs | 0 | Les solutions sont correctes |\n",
"| Itérations EP | 50 EP par fixation, ≈ 2150 au total (2 grilles) | Chaque fixation de cellule requiert 50 itérations EP |\n",
"| Erreurs | 0 \\| Les solutions sont correctes |\n",
"| Itérations EP | 50 EP par fixation, ≈ 2150 au total (2 grilles) \\| Chaque fixation de cellule requiert 50 itérations EP |\n",
"\n",
"**Points clés** :\n",
"1. Le paramètre `NbIterationCells = 2` signifie qu'on fixe 2 cellules par itération\n",
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
date: '2026-09-13'
by: myia-po-2025:CoursIA
python_sha: 4f7c80b40eae94c3f438b3913e64cb3034840261
csharp_sha: da090a35e5255400c66203f61762ee0f4e14fce8
content_python_sha: 47f29e4e84156b40fd717600e4d833004c881d8c9a933a70d5d6ffa22ffe9e23
content_csharp_sha: c5b396e3d3aca5f87ec7d226dfab05675e7d357f608b35f68e99b8441b88f802
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
date: '2026-09-13'
by: myia-po-2025:CoursIA
python_sha: 64bf44d76c163f7cb064add071bfd03ad84ee888
csharp_sha: da090a35e5255400c66203f61762ee0f4e14fce8
content_python_sha: 64d5c0a529c3feb3ede4e592a9116b6c3b70a4c185363f8de0d24b1eadddf2dc
content_csharp_sha: c5b396e3d3aca5f87ec7d226dfab05675e7d357f608b35f68e99b8441b88f802
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
date: '2026-09-13'
by: myia-po-2025:CoursIA
python_sha: d599d4110a060afbbf50c801144edfe1447497ab
csharp_sha: 063e57a69ebbfed4d1cb7061a818e6cd606cf4a6
content_python_sha: cee6c2c540878a2222eeb6fbaefac7e58438ef9998f03c23648643346562e651
content_csharp_sha: 13c608aa1a0a10d6d22533b7800b86790a87a4298038bbd38aae59045e7f7af9
Loading