Skip to content

fix(lean,#17357): Lean-16c -- six affirmations perimees (durees, jours, exercices) #20127

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 2 commits into from
Oct 10, 2026
Merged

fix(lean,#17357): Lean-16c -- six affirmations perimees (durees, jours, exercices) #20127

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b272c3b
fix(lean,#17357): Lean-16c -- six affirmations perimees (durees, jour…
jsboige Oct 9, 2026
b80c0d8
Fix(notebooks,#17357): Lean-16c -- retirer les compteurs "N cellules"…
jsboige Oct 9, 2026
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
25 changes: 13 additions & 12 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16c-Conway-Game-of-Life-Golly.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9551,7 +9551,8 @@
"### Compter le signal produit\n",
"\n",
"Pour rendre le \"calcul\" concret, on mesure la croissance de population : chaque planeur emis ajoute 5 cellules\n",
"vivantes au flux. La courbe de population monte par paliers - chaque palier est un planeur lache dans le circuit."
"vivantes au flux. La courbe n'est pas un escalier monotone : elle oscille fortement au sein de chaque cycle de\n",
"30 generations -- le canon est lui-meme un oscillateur de periode 30 -- et gagne un planeur a chaque cycle."
]
},
{
Expand Down Expand Up @@ -9624,9 +9625,9 @@
"tags": []
},
"source": [
"### Interpretation : lire le graphique en escalier\n",
"### Interpretation : lire le graphique\n",
"\n",
"Chaque palier de la courbe correspond a l'emission d'un planeur (+5 cellules). Le \"step\" est la signature visuelle d'un canon a planeurs. Cette horloge naturelle est le mécanisme fondamental par lequel Life transmet l'information d'un point a un autre -- la base du deuxieme pilier (calcul universel)."
"La courbe oscille fortement d'une generation a l'autre et gagne un planeur par cycle de 30 generations : la progression est *periodique*, et non un escalier monotone. Cette horloge naturelle est le mécanisme fondamental par lequel Life transmet l'information d'un point a un autre -- la base du deuxieme pilier (calcul universel)."
]
},
{
Expand Down Expand Up @@ -15921,7 +15922,7 @@
"| II | Machine de Turing (36 549 cellules) | 1 000 | Le ruban evolue-il ? |\n",
"| III | Gemini (~large) | 100 000 | Première étape vers les 33.6M |\n",
"\n",
"Pour rappel : le simulateur numpy estimait **107 jours** pour Gemini. HashLife va le faire en quelques secondes."
"Pour rappel : le simulateur numpy estimait **~93.2 jours** pour Gemini. HashLife le fera en ~124 s pour les 100 000 premieres generations (et ~1244 s estimes pour les 33.6 M completes)."
]
},
{
Expand Down Expand Up @@ -16157,7 +16158,7 @@
"source": [
"### Interpretation : OTCA Metapixel en HashLife\n",
"\n",
"En **4-5 secondes** de Python pur, HashLife a simule **35 328 generations** d'un motif de 64 691 cellules\n",
"En **~7.3 secondes** de Python pur, HashLife a simule **35 328 generations** d'un motif de plusieurs dizaines de milliers de cellules\n",
"sur une grille implicite de $16384 \\times 16384$. Le simulateur numpy aurait necessite plusieurs minutes\n",
"pour le même calcul (estimation : ~200 ms/generation sur une grille dense de cette taille, soit ~2 heures).\n",
"\n",
Expand Down Expand Up @@ -16279,7 +16280,7 @@
"source": [
"### Interpretation : Machine de Turing en HashLife\n",
"\n",
"La machine de Turing de Rendell (36 549 cellules initiales) evolue sur 1 000 generations en ~4 secondes.\n",
"La machine de Turing de Rendell (un motif spartan de plusieurs dizaines de milliers de cellules) evolue sur 1 000 generations en ~8.6 secondes.\n",
"La population diminue de ~263 cellules : la machine **consomme** des signaux pour effectuer ses transitions.\n",
"Chaque pas de calcul dans Life \"brule\" des planeurs-signaux qui voyagent entre les composants logiques\n",
"(portes AND/OR/NOT implementees en collisions de planeurs).\n",
Expand Down Expand Up @@ -16413,21 +16414,21 @@
"\n",
"| Pilier | Cellules initiales | Generations | Population finale | Temps HashLife | Equiv. numpy |\n",
"|--------|-------------------|-------------|-------------------|---------------|--------------|\n",
"| I - OTCA | 64 691 | 35 328 | ~64 697 | ~4-5s | ~2 heures |\n",
"| II - Turing | 36 549 | 1 000 | ~36 286 | ~4s | ~0.5s (faisable) |\n",
"| III - Gemini | ~large | 100 000 | variable | quelques s | **107 jours** |\n",
"| I - OTCA | 64 691 | 35 328 | ~64 697 | ~7.3s | ~2 heures |\n",
"| II - Turing | 36 549 | 1 000 | ~36 286 | ~8.6s | ~0.5s (faisable) |\n",
"| III - Gemini | ~large | 100 000 | variable | ~124s | **~93.2 jours** |\n",
"\n",
"**Ce qu'on observe** :\n",
"\n",
"1. **OTCA** : la population revient proche de l'initiale après un cycle complet, confirmant le comportement\n",
" oscillatoire predit par `otca_self_emulates`. Le cout est de ~5s pour 35 328 generations d'un motif de 64 691 cellules.\n",
" oscillatoire predit par `otca_self_emulates`. Le cout est de ~7.3s pour 35 328 generations d'un motif de plusieurs dizaines de milliers de cellules.\n",
"\n",
"2. **Turing** : la machine consomme des signaux (population en baisse) au fur et a mesure de ses calculs.\n",
" La simulation HashLife rend concret le theoreme `spartan_adder_correct` : les portes logiques en collisions\n",
" de planeurs fonctionnent reellement.\n",
"\n",
"3. **Gemini** : le flagship. Même 100 000 generations (bien loin des 33.6M du theoreme) sont traitees en\n",
" quelques secondes grace a la compression temporelle de HashLife. Le theoreme `gemini_replicates` affirme\n",
" ~124 s grace a la compression temporelle de HashLife. Le theoreme `gemini_replicates` affirme\n",
" qu'après 33 699 586 generations, le motif est translation de (5, 1) -- la machine s'est copiee.\n",
"\n",
"**Le message** : les trois piliers que le notebook Lean-16b prouve formellement sont des objets **reels** et\n",
Expand Down Expand Up @@ -16538,7 +16539,7 @@
"Les cellules ci-dessous sont des **squelettes a completer** : le notebook s'execute de bout en bout même\n",
"sans les remplir.\n",
"\n",
"L'exercice 4 (Golly / HighLife) est dans la section précédente -- il utilise le webapp Golly plutot que le simulateur numpy."
"L'exercice 1 (Golly / HighLife) est dans la section précédente -- il utilise le webapp Golly plutot que le simulateur numpy."
]
},
{
Expand Down
Loading