Lean-16b : Hommage a John Conway — Game of Life as Computation

Navigation : << Lean-15 Grothendieck | Index | Lean-16c Compagnon Golly >>

Kernel : python3-lean — CPython 3.13 canonique serie Lean (#17476) + Lean 4 via WSL (source de verite formelle, sections 6-7 et annexes D-G)

---

Introduction

John Horton Conway (1937 - 2020) est sans doute le mathematicien qui aura le plus brouille la frontiere entre les jeux et les structures profondes des mathematiques. Cambridge puis Princeton, il a invente le Game of Life en 1970 avec un groupe d’étudiants autour de lui : Michael Guy, Richard Guy, et plusieurs joueurs d’Othello. Sa mort en avril 2020, foudroyee par la COVID, a fait basculer la communaute combinatoire en deuil et accelere les hommages formels.

L’Epic #1151 a ouvert 5 noix moins celebres de Conway en Lean 4 : l’algorithme du Doomsday, la suite Look-and-Say, le langage FRACTRAN, les positions de Nim, le problème de l’ange. Mais l’oeuvre la plus iconique de Conway manquait au catalogue : le Game of Life lui-même.

Ce notebook couvre les phases initiales de l’Epic #1647 (“Hommage Conway : Life-as-Computation”). Il pose les fondations Lean du Game of Life dans conway_lean/Conway/Life.lean, et trace la feuille de route vers les piliers communautaires : Gemini (Wade 2010), OTCA Metapixel (Due 2006), CPU digital (Beluchenko/Stearns 2016).

Une seule source de verite : Life.lean

Le coeur de Life — la règle B3/S23, les patterns, leurs invariants — est défini une seule fois, formellement, dans les modules Lean conway_lean/Conway/Life*.lean. Les simulations Python numpy/matplotlib de ce notebook ne sont pas une seconde définition concurrente : ce sont des illustrations qui donnent l’intuition visuelle (animations, grilles, contours). Quand on veut une certitude (et non une intuition), on interroge directement le .lean : la section 6.1 lance #eval sur les predicats Lean réels, et la section 7 lance lake build. Règle de lecture : le notebook illustre, Life.lean prouve.

Plan

1. La règle Game of Life B3/S23 - définition Python (illustration) + simulation
2. Patterns canoniques : still-lifes, oscillateurs, vaisseaux (blinker, glider)
3. Les 3 piliers communautaires - l’histoire en trois actes (OTCA, machine de Turing, Gemini) et leurs witnesses
4. Demonstration pas-a-pas : blinker et glider animes
5. Turing-completude : Conway 1982, Rendell 2000, Springer 2016
6. La source de vérité Lean : #eval du zoo de patterns, parseur RLE prouvé
7. Vérification : lake build des modules Life + grep sorry honnete
8. Conclusion

Annexes A-G (approfondissements optionnels, en fin de notebook) : les noix Phase 1 déjà portées (A), la logique constructive Spartan (B), l’intuition Hashlife (C), le port Lean en détail — encodage, step, microproofs (D), la limite des string literals (E), le scaffold Pillars.lean (F), la feuille de route de l’Epic #1647 (G).

Exercices

Quatre exercices jalonnent le notebook : compter les voisins de Moore (section 1), classifier un pattern par sa période (section 2), parser un RLE et compter sa population (section 3), et faire vérifier un still-life de votre choix par Lean (section 6). Chaque stub est a completer ; le notebook s’exécute de bout en bout même sans les completer.

Prerequis

• Notions de cellules d’automates cellulaires (utile mais pas indispensable)
• Notebooks Lean-1 a Lean-7 pour les aspects formels (recommande)
• Lean-12 pour le pattern Lake build + WSL

Duree estimée : 60 minutes

1. La règle Game of Life : B3/S23

Le Game of Life est un automate cellulaire déterministe sur le plan infini \(\mathbb{Z}^2\). Chaque cellule a un état binaire (vivante ou morte) et évolue en parallele selon une règle dite B3/S23 :

• Birth (B3) : une cellule morte avec exactement 3 voisins vivants devient vivante.
• Survival (S23) : une cellule vivante avec 2 ou 3 voisins vivants survit ; sinon elle meurt.

Le voisinage utilise est le voisinage de Moore : les 8 cellules entourant directement la cellule consideree (king-move).

Conway a teste plusieurs règles avant de fixer B3/S23 : il cherchait l’équilibre entre extinction rapide et explosion divergente. La règle finale produit un “univers” très riche : motifs stables, oscillateurs, vaisseaux mobiles, générateurs infinis (canons), et finalement universalite Turing.

Implementons-le en Python d’abord, sur un torus fini pour visualisation.

import numpy as np
import matplotlib
matplotlib.use('Agg')
import matplotlib.pyplot as plt
from scipy.signal import convolve2d

def step_gol(grid):
    """Une iteration de B3/S23 sur une grille numpy 2D (avec bord absorbe a 0)."""
    # Compte les voisins via convolution 2D (kernel = 1 partout sauf au centre)
    kernel = np.ones((3, 3), dtype=np.int8)
    kernel[1, 1] = 0
    neighbors = convolve2d(grid, kernel, mode='same', boundary='fill', fillvalue=0)
    # B3 : naissance si 3 voisins ; S23 : survie si 2 ou 3 voisins (et deja vivant)
    new_grid = ((neighbors == 3) | ((grid == 1) & (neighbors == 2))).astype(np.int8)
    return new_grid

# Test rapide : un blinker horizontal sur grille 5x5 devient vertical
g0 = np.zeros((5, 5), dtype=np.int8)
g0[2, 1:4] = 1  # blinker horizontal
g1 = step_gol(g0)

print('Generation 0 (blinker horizontal) :')
print(g0)
print()
print('Generation 1 (blinker vertical apres step B3/S23) :')
print(g1)
print()
# Illustration numérique : apres 2 generations on retrouve le blinker horizontal
g2 = step_gol(g1)
print(f'Generation 2 retombe sur generation 0 : {np.array_equal(g2, g0)}')

Generation 0 (blinker horizontal) :
[[0 0 0 0 0]
 [0 0 0 0 0]
 [0 1 1 1 0]
 [0 0 0 0 0]
 [0 0 0 0 0]]

Generation 1 (blinker vertical apres step B3/S23) :
[[0 0 0 0 0]
 [0 0 1 0 0]
 [0 0 1 0 0]
 [0 0 1 0 0]
 [0 0 0 0 0]]

Generation 2 retombe sur generation 0 : True

Interpretation : le blinker comme oscillateur période 2

Le blinker est le plus petit oscillateur non-trivial de Life : 3 cellules alignees. Toutes les 2 generations, il oscille entre orientation horizontale et verticale. La vérification g2 == g0 ci-dessus est une illustration numérique sur grille bornee : elle montre la periodicite sur un cas concret, elle ne la prouve pas (une seule grille, finie).

\[\text{step}^2(\text{blinker}) = \text{blinker} \quad \text{(propriété illustree ici, prouvée en Lean)}\]

Le théorème correspondant — la verite formelle, valable sur le plan infini \(\mathbb{Z}^2\) — vit dans la source unique conway_lean/Conway/Life.lean :

theorem blinker_period_two : isOscillator blinker_h 2 = true := by native_decide

Le predicat isOscillator g n := evolve n g == g retourne un Bool sur le type List (Int x Int) ; native_decide le compile en code natif et tranche true en un éclair (cf section 9 pour le choix List plutot que Finset). Le notebook illustre ; Life.lean prouve.

Exercice 1 : compter les voisins de Moore

Le coeur de la règle B3/S23, c’est le comptage des voisins vivants dans le voisinage de Moore (les 8 cellules adjacentes, king-move). La fonction step_gol ci-dessus delegue ce comptage a scipy.signal.convolve2d ; pour bien comprendre la règle, on le refait a la main.

A vous : implementez count_live_neighbors(grid, i, j) qui compte les voisins vivants de la cellule (i, j) sans convolution, en traitant les cellules hors grille comme mortes. Une fois cette brique en place, naissance (== 3) et survie (== 2 or == 3) en decoulent directement.

import numpy as np

def count_live_neighbors(grid, i, j):
    """Compte les voisins vivants (voisinage de Moore, king-move) de la cellule (i, j).

    Les cellules hors de la grille comptent comme mortes (bord absorbant).
    C'est l'opération fondamentale dont decoulent naissance (B3) et survie (S23).

    Args:
        grid: np.ndarray 2D de 0/1
        i, j: indices (ligne, colonne) de la cellule centrale
    Returns:
        int : nombre de voisins vivants parmi les 8 cellules adjacentes
    """
    # TODO étudiant : parcourir les 8 offsets de Moore et sommer les cellules vivantes
    # Indice : for di in (-1, 0, 1): for dj in (-1, 0, 1): ... ignorer (0, 0)
    # Indice : ne compter que si 0 <= i+di < n_rows et 0 <= j+dj < n_cols (sinon hors grille = mort)
    return None  # TODO étudiant : remplacer par le compte des voisins vivants

# Vérification (a activer une fois implemente) :
# g = np.array([[1, 1, 0], [0, 1, 0], [0, 0, 1]], dtype=np.int8)
# print("Voisins vivants de (1,1) :", count_live_neighbors(g, 1, 1), "(attendu : 3)")
_demo = count_live_neighbors(np.zeros((3, 3), dtype=np.int8), 1, 1)
print("Exercice 1 a completer" if _demo is None else f"count_live_neighbors implemente : {_demo}")

Exercice 1 a completer

2. Patterns canoniques du Game of Life

Trois grandes familles de patterns ont ete identifiees des les premières semaines après l’invention de Life (octobre 1970, Cambridge) :

Famille	Définition	Exemples
Still life	step(g) = g	Block, beehive, loaf, boat, ship
Oscillator	step^n(g) = g pour un certain n > 0	Blinker (n=2), toad (n=2), beacon (n=2), pulsar (n=3), pentadecathlon (n=15)
Spaceship	step^n(g) = shift_v(g) pour v != 0	Glider (n=4, v=(1,-1)), LWSS / MWSS / HWSS, Gemini (n=33 699 586)

Le glider (Richard Guy, 1970) est le plus iconique : 5 cellules qui se deplacent en diagonale, période 4, vitesse \(c/4\) ou \(c\) est la vitesse limite de propagation de Life. C’est le “photon” de l’univers de Conway.

Visualisons quelques generations.

def plot_grid(ax, grid, title, gen):
    """Affiche une grille binaire dans un axe matplotlib."""
    ax.imshow(grid, cmap='Greys', interpolation='nearest', vmin=0, vmax=1)
    ax.set_title(f'{title}\nGen {gen}', fontsize=10)
    ax.set_xticks([])
    ax.set_yticks([])
    ax.grid(False)

def simulate_pattern(pattern, n_steps, padding=2):
    """Encadre le pattern et le simule n_steps fois sans bord absorbant."""
    # Trouver la bbox
    rows, cols = pattern.shape
    big = np.zeros((rows + 2 * padding, cols + 2 * padding), dtype=np.int8)
    big[padding:padding+rows, padding:padding+cols] = pattern
    frames = [big.copy()]
    for _ in range(n_steps):
        big = step_gol(big)
        frames.append(big.copy())
    return frames

# Block (still life)
block = np.array([[1, 1], [1, 1]], dtype=np.int8)
block_frames = simulate_pattern(block, 2, padding=3)

# Blinker (period 2)
blinker = np.array([[1, 1, 1]], dtype=np.int8)
blinker_frames = simulate_pattern(blinker, 4, padding=2)

# Glider (period 4, displacement (1,1))
glider = np.array([
    [0, 1, 0],
    [0, 0, 1],
    [1, 1, 1],
], dtype=np.int8)
glider_frames = simulate_pattern(glider, 4, padding=4)

# Affichage
fig, axes = plt.subplots(3, 5, figsize=(11, 7))
for i, frame in enumerate(block_frames[:3]):
    plot_grid(axes[0, i], frame, 'Block (still life)', i)
for i in range(3, 5):
    axes[0, i].axis('off')
for i, frame in enumerate(blinker_frames[:5]):
    plot_grid(axes[1, i], frame, 'Blinker (period 2)', i)
for i, frame in enumerate(glider_frames[:5]):
    plot_grid(axes[2, i], frame, 'Glider (period 4, diag)', i)

plt.tight_layout()
import io
from IPython.display import Image, display
buf = io.BytesIO()
fig.savefig(buf, format='png', dpi=80, bbox_inches='tight')
plt.close(fig)
display(Image(data=buf.getvalue()))
print()
print('Illustrations numeriques (grille bornee) :')
print(f'  Block      : step(block)   == block         ? {np.array_equal(block_frames[0], block_frames[1])}')
print(f'  Blinker    : step^2(blink) == blink         ? {np.array_equal(blinker_frames[0], blinker_frames[2])}')
# Le glider est translate : on compare les bbox des cellules vivantes
def live_offsets(g):
    ys, xs = np.where(g == 1)
    if len(ys) == 0:
        return set()
    miny, minx = ys.min(), xs.min()
    return set(zip(ys - miny, xs - minx))
print(f'  Glider     : step^4(glider) ~= shift(glider) ? {live_offsets(glider_frames[0]) == live_offsets(glider_frames[4])}')

Illustrations numeriques (grille bornee) :
  Block      : step(block)   == block         ? True
  Blinker    : step^2(blink) == blink         ? True
  Glider     : step^4(glider) ~= shift(glider) ? True

Interpretation : 3 invariants illustres numeriquement

Pattern	Type	Propriété illustree (verif. numpy, grille bornee)
Block (2x2)	Still life	\(\text{step}(\text{block}) = \text{block}\)
Blinker (1x3)	Oscillator période 2	\(\text{step}^2(\text{blinker}) = \text{blinker}\)
Glider (3x3 L-shape)	Spaceship période 4	\(\text{step}^4(\text{glider}) = \text{shift}_v(\text{glider})\)

Ces vérifications numpy illustrent le comportement sur une grille finie ; les théorèmes formels correspondants (block_still_life, blinker_period_two, glider_spaceship) sont prouves par native_decide dans la source unique conway_lean/Conway/Life.lean (section 6, détails en Annexe D). Le notebook donne l’intuition visuelle ; le .lean porte la certitude mathematique sur le plan infini.

Phase 2 (PR #1975) : les modules Spaceships.lean et Oscillators.lean ajoutent de nouveaux théorèmes, dont le pulsar (période 3) et le pentadecathlon (période 15) — deux patterns initialement consideres “borderline” pour native_decide mais qui passent avec succes. On les évalue directement en section 6.1.

Patterns plus grands explores en Phases ulterieures : Gosper glider gun (genere des gliders a l’infini), pufferfishes, LWSS/MWSS/HWSS (déjà prouves), Gemini replicator, OTCA Metapixel. Voir LifeWiki pour le catalogue complet.

Exercice 2 : classifier un pattern par sa période

Les trois familles de la section 2 se distinguent par leur période : un still-life a la période 1 (step(g) == g), un oscillateur a une période n > 1 fixe, et un vaisseau ne revient jamais a sa position d’origine (il se deplace).

A vous : implementez detect_period(pattern, max_period=20) qui simule le pattern et retourne la plus petite période n telle que la grille redevienne identique a position fixe, ou None si elle ne revient pas (cas du vaisseau). Reutilisez simulate_pattern et step_gol. C’est l’analogue empirique Python du predicat formel isOscillator de Life.lean.

def detect_period(pattern, max_period=20, padding=4):
    """Detecte la période d'un pattern a position fixe (still-life = 1, oscillateur = n).

    Un vaisseau (glider) ne revient jamais a sa position d'origine : on attend `None`.
    Reutilise `simulate_pattern` et `step_gol` definis en section 2.

    Args:
        pattern: np.ndarray 2D de 0/1
        max_period: borne supérieure de recherche de période
        padding: marge autour du pattern (evite le bord absorbant)
    Returns:
        int : période minimale n in [1, max_period] telle que step^n(g) == g, sinon None
    """
    frames = simulate_pattern(pattern, max_period, padding=padding)
    # TODO étudiant : trouver le plus petit n >= 1 tel que frames[n] soit identique a frames[0]
    # Indice : for n in range(1, max_period + 1): if np.array_equal(frames[n], frames[0]): return n
    return None  # TODO étudiant : remplacer par la période detectee (ou None si aucune)

# Vérifications (a activer une fois implemente) :
# print("Block   ->", detect_period(block),   "(attendu : 1, still-life)")
# print("Blinker ->", detect_period(blinker), "(attendu : 2, oscillateur)")
# print("Glider  ->", detect_period(glider),  "(attendu : None, c'est un vaisseau qui se deplace)")
_p = detect_period(blinker)
print("Exercice 2 a completer" if _p is None else f"detect_period(blinker) = {_p}")

Exercice 2 a completer

3. Les 3 piliers communautaires : une histoire en trois actes

L’Epic #1647 est autant un hommage a Conway qu’a la communaute Life. Depuis cinquante ans, des amateurs et des chercheurs ont construit dans cet automate des objets de plus en plus ambitieux. Trois d’entre eux forment une belle histoire, qu’on peut raconter comme une montee en puissance autour d’une seule question : jusqu’ou Life peut-elle se prendre elle-même pour objet ?

• Acte I - se refleter. Une cellule geante qui est une cellule de Life : l’OTCA Metapixel. Life calcule Life.
• Acte II - se reproduire. Un motif qui fabrique sa propre copie a partir d’un plan : Gemini. Life se replique.
• Acte III - calculer. Un motif qui exécute un programme : le CPU digital de Beluchenko/Stearns (2016), puis le CPU 8 bits de Carlini (2020). Life calcule.

Mises bout a bout, ces trois étapes donnent la cascade vertigineuse de la fin de section : Life calcule Life qui calcule un CPU.

Chaque acte est associe a un witness concret : un fichier RLE (Run-Length Encoded), le format standard de la communaute, qu’on va télécharger et regarder pour de vrai. Un fichier RLE tient en trois parties :

• des lignes de commentaire prefixees # : #N le nom, #O l’auteur et l’annee, #C une description ;
• une ligne d’en-tete x = <largeur>, y = <hauteur>, rule = B3/S23 ;
• un corps compresse : o = cellule vivante, b = cellule morte, un entier prefixe une repetition, $ termine une rangee, ! termine le motif.

On lit ces witnesses depuis le miroir public copy.sh/life/examples/. Tout le code reseau ci-dessous est protege : si un téléchargement echoue, le notebook l’annonce et continue sans erreur.

Chargeons d’abord la boite a outils, puis levons le rideau sur l’Acte I.

# Boite a outils RLE : télécharger, parser et afficher les witnesses de la communaute Life.
import os, re, tempfile, urllib.request
import io
import numpy as np
import matplotlib.pyplot as plt
from IPython.display import Image, display

MIRROR = "https://copy.sh/life/examples/"
RLE_CACHE = os.path.join(tempfile.gettempdir(), "lean14_rlecache")


def fetch_rle(name, timeout=60):
    """Telecharge un witness RLE depuis le miroir copy.sh (avec cache disque).
    Retourne le texte, ou None si le reseau echoue (le notebook continue)."""
    os.makedirs(RLE_CACHE, exist_ok=True)
    fp = os.path.join(RLE_CACHE, name)
    if os.path.exists(fp) and os.path.getsize(fp) > 0:
        with open(fp, "r", encoding="utf-8", errors="replace") as f:
            return f.read()
    try:
        req = urllib.request.Request(MIRROR + name, headers={"User-Agent": "Mozilla/5.0"})
        data = urllib.request.urlopen(req, timeout=timeout).read().decode("utf-8", "replace")
        with open(fp, "w", encoding="utf-8") as f:
            f.write(data)
        return data
    except Exception as exc:
        print(f"  witness indisponible ({name}) : {type(exc).__name__} - le notebook continue")
        return None


def parse_rle(text):
    """Parse un RLE. Retourne (W, H, xs, ys, comments) ; xs/ys = coords des cellules vivantes."""
    comments, header, body = [], None, []
    for ln in text.splitlines():
        s = ln.strip()
        if not s:
            continue
        if s.startswith("#"):
            comments.append(s)
        elif header is None and s[:1].lower() == "x":
            header = s
        else:
            body.append(s)
    m = re.search(r"x\s*=\s*(\d+).*?y\s*=\s*(\d+)", header or "", re.I)
    W = int(m.group(1)) if m else 0
    H = int(m.group(2)) if m else 0
    xs, ys, x, y = [], [], 0, 0
    for n, tag in re.findall(r"(\d*)([bo$!])", "".join(body)):
        c = int(n) if n else 1
        if tag == "b":
            x += c
        elif tag == "o":
            xs.extend(range(x, x + c)); ys.extend([y] * c); x += c
        elif tag == "$":
            y += c; x = 0
        elif tag == "!":
            break
    return W, H, np.array(xs, dtype=np.int64), np.array(ys, dtype=np.int64), comments


def show_header(name, W, H, xs, ys, comments):
    """Affiche les metadonnees d'un witness : nom, auteur, description, taille, population."""
    print(f"witness : {name}")
    for c in comments:
        if c[:2] in ("#N", "#O", "#C"):
            print("   ", c[:88])
    pop = f"{len(xs):,}".replace(",", " ")
    print(f"    en-tete : {W} x {H}    cellules vivantes : {pop}")
    if len(xs):
        print(f"    bbox reelle : x[{xs.min()}..{xs.max()}] y[{ys.min()}..{ys.max()}]")


def render_pattern(xs, ys, title, dense_limit=6_000_000, sub=80_000):
    """Affiche un witness. Petit motif -> grille dense (imshow) ; tres grand -> nuage 2 panneaux
    (vue d'ensemble sous-echantillonnee + zoom sur un moteur de construction)."""
    if len(xs) == 0:
        print("    (rien a afficher)"); return
    minx, maxx, miny, maxy = xs.min(), xs.max(), ys.min(), ys.max()
    if (maxx - minx + 1) * (maxy - miny + 1) <= dense_limit:
        arr = np.zeros((maxy - miny + 1, maxx - minx + 1), dtype=bool)
        arr[ys - miny, xs - minx] = True
        fig, ax = plt.subplots(figsize=(6, 6))
        ax.imshow(arr, cmap="binary", interpolation="nearest")
        ax.set_title(title, fontsize=10); ax.axis("off")
    else:
        fig, (a0, a1) = plt.subplots(1, 2, figsize=(11, 5.5))
        if len(xs) > sub:
            idx = np.linspace(0, len(xs) - 1, sub).astype(np.int64)
            a0.scatter(xs[idx], ys[idx], s=0.05, c="black", marker=".", linewidths=0)
        else:
            a0.scatter(xs, ys, s=0.05, c="black", marker=".", linewidths=0)
        a0.set_aspect("equal"); a0.invert_yaxis()
        a0.set_title(f"{title}\nvue d'ensemble : le ruban oblique", fontsize=9)
        xthr = minx + 0.003 * (maxx - minx)
        tip = xs < xthr
        tx0, tx1, ty0, ty1 = xs[tip].min(), xs[tip].max(), ys[tip].min(), ys[tip].max()
        pad = int(0.15 * max(tx1 - tx0, ty1 - ty0)) + 30
        m = (xs >= tx0 - pad) & (xs <= tx1 + pad) & (ys >= ty0 - pad) & (ys <= ty1 + pad)
        a1.scatter(xs[m], ys[m], s=2.0, c="black", marker=".", linewidths=0)
        a1.set_aspect("equal"); a1.invert_yaxis()
        a1.set_title(f"zoom : un moteur de construction\n{int(m.sum())} cellules", fontsize=9)
    plt.tight_layout()
    buf = io.BytesIO()
    fig.savefig(buf, format="png", dpi=90, bbox_inches="tight")
    plt.close(fig)
    display(Image(data=buf.getvalue()))


# Demonstration deterministe (sans reseau) : un planeur en RLE.
_glider = "x = 3, y = 3, rule = B3/S23\nbob$2bo$3o!"
_W, _H, _xs, _ys, _ = parse_rle(_glider)
print("Boite a outils RLE prete.")
print(f"Test parser sur un planeur : en-tete {_W}x{_H}, {len(_xs)} cellules vivantes "
      f"aux coordonnees {sorted(zip(_xs.tolist(), _ys.tolist()))}")

Boite a outils RLE prete.
Test parser sur un planeur : en-tete 3x3, 5 cellules vivantes aux coordonnees [(0, 2), (1, 0), (1, 2), (2, 1), (2, 2)]

Acte I - SELF-EMULATION : OTCA Metapixel (Brice Due, 2006)

• Auteur / annee : Brice Due, 2006
• Taille : 2048 x 2048 cellules par metapixel
• Tick interne : 35 328 generations = 1 “OTCA-tick” = 1 generation au niveau macro
• Source : conwaylife.com/wiki/OTCA_metapixel

Le premier prodige, c’est l’auto-emulation. Brice Due construit une cellule geante : un carré de plusieurs millions de cellules ordinaires qui, vu de loin, se comporte exactement comme une seule cellule de Life. Elle a deux états (allumee / eteinte), elle observe ses huit voisines geantes, et toutes les 35 328 generations elle applique la règle B3/S23 a l’échelle macro. Pavez le plan de metapixels et vous obtenez un Game of Life a l’interieur d’un Game of Life, a une échelle 2048 fois plus grande et 35 328 fois plus lente.

C’est Life calcule Life : une self-similarite formelle, l’analogue cellulaire d’un interpreteur qui s’exécute lui-même. C’est aussi la cle de voute de l’Epic, car combinee a l’Acte II elle donne Life calcule Life qui calcule un CPU - une Turing-completude par construction, en cascade.

Caractéristique	Valeur
Auteur / annee	Brice Due, 2006
Pattern RLE	otcametapixel.rle
Taille (en-tete)	2 048 x 2 048
Generations par tick	35 328
Niveau quadtree (estimé)	~9
Population (initiale)	~50 000 cellules
Ce qu’il démontre	Life emule Life : chaque metapixel = 1 cellule B3/S23 macro

Théorème cible Lean (Phase 7, Epic #1647) :

theorem otca_self_emulates : forall g, is_bounded g ->
    step^[35328] (zoom_otca g) = zoom_otca (step g) := by native_decide

Regardons le witness : un metapixel, soit une cellule de Life faite de cellules de Life.

# Acte I : OTCA Metapixel (Brice Due, 2006) - la cellule qui est une cellule.
txt = fetch_rle("otcametapixel.rle")
if txt is not None:
    W, H, xs, ys, com = parse_rle(txt)
    show_header("otcametapixel.rle", W, H, xs, ys, com)
    render_pattern(xs, ys, "OTCA Metapixel (Brice Due, 2006) - une cellule B3/S23 geante")

witness : otcametapixel.rle
    #N OTCA metapixel
    #O Brice Due
    #C A unit cell that is capable of emulating any Life-like cellular aut
    #C omaton. Constructed in 2006.
    #C www.conwaylife.com/wiki/index.php?title=OTCA_metapixel
    en-tete : 2058 x 2058    cellules vivantes : 64 691
    bbox reelle : x[0..2057] y[0..2057]

Acte II - CALCUL : machine de Turing (Rendell, 2000) et calculateurs numériques

• Paul Rendell, avril 2000 : la première machine de Turing explicite construite dans Life - le witness telechargeable ci-dessous.
• Nicolay Beluchenko / Andy Stearns, 2016 : un CPU digital programmable construit a partir d’OTCA metapixels, executant un cycle en 1 048 576 generations. Ce CPU est le temoin cpu_witness declare dans Conway.Life.Pillars.lean (Phase 8 cible).
• Nicholas Carlini, 2020 : un CPU 8 bits complet (ROM, RAM, ALU, registres, horloge), de l’ordre de \(10^6\) cellules - indépendant du CPU de Beluchenko/Stearns. Trop massif pour être rendu ou decide ici, c’est le sommet de la discipline.
• Adam P. Goucher, additionneur Spartan : environ 5 000 cellules, cible pragmatique pour la preuve Lean.

Le deuxieme prodige, c’est le calcul proprement dit. Des 1970, Conway conjecturait que Life était Turing-complète ; Paul Rendell l’a prouve par construction en 2000 en batissant une vraie machine de Turing - ruban, tete de lecture, table de transitions - entierement en cellules B3/S23. Vingt ans plus tard, Carlini est alle au bout de l’idee avec un microprocesseur 8 bits fonctionnel.

Caractéristique	Machine de Turing (Rendell)	CPU digital (Beluchenko/Stearns)
Auteur / annee	Paul Rendell, 2000	Beluchenko / Stearns, 2016
Pattern RLE	turingmachine.rle	(integre dans OTCA metapixels)
Generations par cycle	Variable (depend du programme)	1 048 576
Niveau quadtree (estimé)	~10	~12
Ce qu’il démontre	Turing-completude constructive	CPU programmable dans Life

Pour la preuve formelle, on ne vise pas le CPU complet (le binaire native_decide n’y tiendrait pas) : on commence par l’additionneur Spartan de Goucher, assez petit pour être decide, et on remonte si la machine suit.

Théorème cible Lean (additionneur, Phase 8) :

theorem spartan_adder_correct : forall (a b : Fin 256),
    read_output (step^[adder_cycle] (adder_init a b)) = a + b := by native_decide

Le witness ci-dessous est la machine de Rendell : un objet qu’on peut tenir dans une grille et regarder.

# Acte II : machine de Turing de Paul Rendell (2000) - le calcul rendu visible.
txt = fetch_rle("turingmachine.rle")
if txt is not None:
    W, H, xs, ys, com = parse_rle(txt)
    show_header("turingmachine.rle", W, H, xs, ys, com)
    render_pattern(xs, ys, "Machine de Turing dans Life (Paul Rendell, 2000)")

witness : turingmachine.rle
    #N Turing machine
    #O Paul Rendell
    #C A pattern capable of turing-complete computation. Created in April
    #C 2000.
    #C www.conwaylife.com/wiki/index.php?title=Turing_machine
    en-tete : 1714 x 1647    cellules vivantes : 36 549
    bbox reelle : x[0..1713] y[0..1646]

Acte III - REPLICATION : Gemini (Andrew Wade, 2010)

• Auteur / annee : Andrew J. Wade, 30 juillet 2010
• Période : 33 699 586 generations pour produire une copie complète
• Deplacement : knightship oblique, direction (5, 1)
• Source : conwaylife.com/wiki/Gemini

Le troisieme prodige - le bouquet final de notre histoire - c’est l’auto-reproduction. Maintenant que Life sait s’emuler elle-même (Acte I) et calculer (Acte II), il lui reste le geste le plus spectaculaire : se recopier. Gemini est le premier self-replicator du Game of Life : un motif qui construit une copie de lui-même, detruit l’original, et recommence - en se deplacant en biais a la maniere d’un cavalier d’echecs. C’est la realisation, dans Life, du constructeur universel imagine par von Neumann : une machine qui lit un plan et fabrique l’objet decrit, le plan se decrivant lui-même.

Sa structure se lit directement sur le witness. L’essentiel de sa masse n’est pas un mécanisme, c’est de l’information : un long ruban oblique qui encode, glider après glider, le plan de la copie. Aux extremites, deux moteurs de construction (les bras) lisent le ruban et batissent la replique. Le panneau de zoom ci-dessous isole un de ces moteurs ; la vue d’ensemble montre le ruban qui file en diagonale. La population affichée (plusieurs centaines de milliers de cellules) est donc surtout du plan, pas de la machinerie.

Caractéristique	Valeur
Auteur / annee	Andrew J. Wade, 2010
Pattern RLE	gemini.rle
Generations par replication	33 699 586
Deplacement	Knightship oblique, direction (5, 1)
Niveau quadtree (estimé)	~14
Population (initiale)	~846 000 cellules
Ce qu’il démontre	Auto-replication : Gemini construit sa copie, detruit l’original, recommence

Théorème cible Lean (Phase 6, Epic #1647) :

theorem gemini_replicates :
    evolve 33699586 gemini = shift (5, 1) gemini := by native_decide

Le witness est trop vaste pour une grille dense : on l’affiche en nuage de points.

# Acte III : Gemini (Andrew Wade, 2010) - le self-replicator oblique.
txt = fetch_rle("gemini.rle")
if txt is not None:
    W, H, xs, ys, com = parse_rle(txt)
    show_header("gemini.rle", W, H, xs, ys, com)
    render_pattern(xs, ys, "Gemini (Andrew Wade, 2010) - self-replicator oblique")

witness : gemini.rle
    #CXRLE Pos=-2753,-4702 Gen=0
    #C A (5120,1024)c/33699586 universal constructor based spaceship.
    #C
    #C      The two construction arms and single destruction arm in each
    #C replicator pattern are based on a design by Paul Chapman and
    #C Dave Greene.
    #C
    #C      At least two replicator patterns are active at any one time:
    #C one at the top left that reflects the instruction tape to the
    #C bottom right, and one at the bottom right that reflects the
    #C instruction tape back to the top left. The two reflections offset
    #C the tape by 4096 cells, ready for the next copy of the replicator
    #C pattern. The replicators are all identical, and some of the
    #C circuitry is only active in the top left or the bottom right
    #C replicators.
    #C
    #C Andrew Wade, May 2, 2010
    en-tete : 4217807 x 4220191    cellules vivantes : 846 278
    bbox reelle : x[0..4217806] y[0..4220190]

La cascade : Life calcule Life qui calcule un CPU

Remettons les trois actes dans l’ordre ou on vient de les voir :

Acte	Witness	Prouesse	En une phrase
I	OTCA Metapixel (Due, 2006)	self-emulation	Life se simule elle-même
II	Turing / calculateurs (2000-2020)	calcul universel	Life calcule n’importe quoi
III	Gemini (Wade, 2010)	self-replication	Life se recopie elle-même

La beaute de l’histoire tient a leur emboitement, et l’ordre est une montee en puissance. L’Acte I prouve que Life peut faire tourner Life. L’Acte II prouve que Life peut faire tourner un ordinateur. En composant les deux, on obtient un ordinateur a l’interieur d’un metapixel : Life calcule Life qui calcule un CPU. Et l’Acte III, le bouquet final, garantit qu’une telle construction peut se reproduire toute seule - on tient la, en cellules vivantes, les trois ingredients de von Neumann d’une machine auto-reproductrice et universelle.

C’est pourquoi ces witnesses sont les piliers de l’Epic #1647 : chacun est une preuve par construction, et leur composition est l’argument de Turing-completude le plus tangible qu’on puisse donner du Game of Life.

Noms de théorèmes : narration vs implémentation

Les théorèmes cibles ci-dessus (otca_self_emulates, spartan_adder_correct, gemini_replicates) sont des noms prospectifs qui servent le recit pedagogique. Les noms réels dans le code Lean suivent la convention <pattern>_witness :

Nom prospectif (section 3)	Nom réel dans Pillars.lean	Statut
otca_self_emulates	otca_metapixel_witness	prouve (vide) - Phase 7 réel
spartan_adder_correct	cpu_witness (Beluchenko/Stearns)	prouve (vide) - Phase 8 réel
gemini_replicates	gemini_witness	prouve (vide) - Phase 6 réel
—	unitcell_witness (Beluchenko 2011)	prouve (vide) - Phase 8 réel

Statut compile = prouve contre grilles vides. Les temoins compilent sans sorry : otcaInitial / otcaTarget etc. sont des grilles vides (([] : Grid)), donc evolveHashlifeFastMemo N [] = [] est prouvé trivialement par le lemme evolveHashlifeFastMemo_empty. Aucun axiome n’est admis. La preuve réelle - le pattern RLE charge (OTCA 70 KB, Gemini plusieurs MB) pousse dans native_decide - reste l’objectif des Phases 6-8 une fois la memoization Hashlife en place.

Le temoin (unitcell_witness, UnitCell de Beluchenko, 4096 generations) n’apparait pas dans le recit des trois actes : c’est un metapixel plus petit que l’OTCA, plus accessible comme première cible native_decide. Il est integrallement défini dans Pillars.lean et constitue un jalon intermediaire naturel avant l’OTCA complète.

Chaque preuve réelle est prevue comme un seul by native_decide une fois la memoization Hashlife en place.

Exercice 3 : parser un RLE et compter sa population

Les trois piliers (OTCA, Turing, Gemini) ne sont que les sommets les plus emblematiques d’un catalogue immense. Des centaines d’autres patterns celebres vivent sur LifeWiki et le miroir copy.sh/life/examples/ : canons a planeurs, spacefillers, grow-by-tail patterns…

A vous : implementez explorer_witness(nom_rle) qui telecharge un witness, le parse avec la boite a outils de la section 3, puis retourne un tuple (population, (largeur_bbox, hauteur_bbox)) decrivant le motif. La fonction doit gerer le cas ou le téléchargement echoue (reseau indisponible) en retournant None.

Étapes : 1. Appeler fetch_rle(nom_rle) pour obtenir le texte RLE. 2. Appeler parse_rle(texte) pour extraire les coordonnees des cellules vivantes. 3. Calculer la population (len(xs)) et les dimensions de la bounding box (maxx - minx + 1, maxy - miny + 1). 4. Retourner (population, (largeur_bbox, hauteur_bbox)) ou None si le téléchargement echoue.

Idees de witnesses : "gosperglidergun.rle" (canon a planeurs de Gosper, 1970), "spacefiller.rle" (remplit le plan a vitesse linéaire), "max.rle" (machine “Max” de Callahan, croissance quadratique).

# Exercice 3 : parser un RLE et compter sa population + bounding box.
# TODO étudiant : utilisez fetch_rle et parse_rle de la section 3.
# Etape 1 : télécharger le witness avec fetch_rle(nom).
# Etape 2 : le parser avec parse_rle(texte) -> (W, H, xs, ys, comments).
# Etape 3 : calculer population et bbox.

def explorer_witness(nom_rle: str) -> dict:
    result = None  # TODO étudiant
    return result

print("Exercice a completer")

Exercice a completer

4. Demonstration : simulation pas-a-pas du blinker et du glider

Affichage explicite de toutes les generations sur 8 steps, pour bien visualiser la periodicite (blinker période 2) et le deplacement (glider période 4).

# Blinker - 8 generations
blinker8 = simulate_pattern(blinker, 8, padding=2)
# Glider - 8 generations (= 2 périodes complète)
glider8 = simulate_pattern(glider, 8, padding=5)

fig, axes = plt.subplots(2, 9, figsize=(15, 4))
for i in range(9):
    plot_grid(axes[0, i], blinker8[i], 'Blinker', i)
    plot_grid(axes[1, i], glider8[i], 'Glider', i)
plt.suptitle('Blinker (period 2) vs Glider (period 4, shift (1,1))', fontsize=11)
plt.tight_layout()
buf2 = io.BytesIO()
fig.savefig(buf2, format='png', dpi=80, bbox_inches='tight')
plt.close(fig)
display(Image(data=buf2.getvalue()))
print()
# Illustrations numériques (les preuves formelles sont dans Life.lean)
print('Illustrations de periodicite :')
for k in [2, 4, 6, 8]:
    eq = np.array_equal(blinker8[k], blinker8[0])
    print(f'  step^{k}(blinker) == blinker ? {eq}')
print()
print('Illustrations de deplacement :')
for k in [4, 8]:
    eq_offsets = (live_offsets(glider8[k]) == live_offsets(glider8[0]))
    print(f'  step^{k}(glider) ~= shift(glider) (memes offsets) ? {eq_offsets}')

Illustrations de periodicite :
  step^2(blinker) == blinker ? True
  step^4(blinker) == blinker ? True
  step^6(blinker) == blinker ? True
  step^8(blinker) == blinker ? True

Illustrations de deplacement :
  step^4(glider) ~= shift(glider) (memes offsets) ? True
  step^8(glider) ~= shift(glider) (memes offsets) ? True

Interpretation : structure spatio-temporelle

Le blinker reproduit exactement sa configuration toutes les 2 generations - c’est la définition d’un oscillateur. Le glider reproduit sa silhouette (mêmes offsets relatifs entre cellules) toutes les 4 generations, mais translatee de \((1, 1)\) - c’est un vaisseau de vitesse \(c/4\) ou \(c\) est la vitesse limite de Life.

Ces deux patterns sont les briques élémentaires des constructions ulterieures : - Les blinkers et autres oscillateurs servent d’horloges dans le CPU digital (Beluchenko/Stearns) ou le ribosome Gemini. - Les gliders servent de signaux (bits) transportes sur des canaux periodiques.

5. Turing-completude du Game of Life

La Turing-completude du Game of Life a ete conjecturee par Conway lui-même des 1970 et prouvée constructivement par Paul Rendell en 2000.

Sequence historique

Annee	Auteur	Résultat
1970	Conway	Conjecture l’universalite
1982	Conway / Berlekamp / Guy	Winning Ways vol. 2 : argument heuristique d’universalite
2000	Paul Rendell	Construction explicite d’une machine de Turing dans Life
2010	Wade	Universal constructor (Gemini)
2016	Rendell	Springer, Turing Machine Universality of the Game of Life (these PhD)
2020	Carlini	8-bit computer working in Life

Stratégie de preuve en Lean (Phase 9 de l’Epic)

L’argument formel se decompose ainsi :

1. Prouver la correction d’une porte NAND dans Life (e.g. Rendell 2000) :

   theorem nand_gate_correct :
       forall a b, evolve N (nand_pattern a b) contains output (¬(a ∧ b))

2. Admettre comme axiome documente (avec reference Sipser/Rendell) que NAND universel + composition => Turing-complète :

   axiom nand_universal_implies_turing_complete :
       (forall a b, computes_nand (g a b)) -> turing_complete Grid step

3. En deduire le théorème final :

   theorem game_of_life_turing_complete :
       turing_complete Grid step :=
     nand_universal_implies_turing_complete nand_gate_correct

Note : Pilier 2 (OTCA Metapixel) donne déjà une forme constructive de Turing-completude (Life simule Life qui simule un CPU), donc le axiom NAND est redondant mais pedagogiquement utile.

6. La source de vérité : le port Lean 4

Tout ce que les sections précédentes ont illustre en Python vit formellement dans conway_lean/Conway/Life.lean et ses modules : la règle B3/S23 (step), les prédicats isStillLife / isOscillator / isSpaceship (tous Bool, pour native_decide), les patterns canoniques et leurs microproofs — block, blinker, glider, LWSS/MWSS/HWSS, pulsar, pentadecathlon — tous prouvés, sans sorry.

Cette section interroge la source de vérité en direct : statistiques des modules (ci-dessous), #eval du zoo de patterns (6.1), le parseur RLE prouvé (6.2), puis lake build en section 7. Le détail de l’encodage — pourquoi List (Int × Int) plutôt que Finset, le step sur liste triée, les microproofs ligne à ligne — est en Annexe D.

import sys
from pathlib import Path

# Cross-platform Lean utilities (Epic #2314)
sys.path.insert(0, str(Path.cwd()))
from lean_notebook_utils import (
    find_lean_project, get_lean_project_path,
    run_lake, count_sorry, run_lean_snippet,
)

# Backward-compatible aliases for cells later in this notebook
WIN_LEAN_PROJECT = find_lean_project('conway_lean')
LEAN_PROJECT = get_lean_project_path('conway_lean')

def wsl(cmd, timeout=60):
    """Exécute a bash command inside WSL Ubuntu (backward-compatible wrapper)."""
    return run_lake(LEAN_PROJECT, cmd, timeout=timeout) if False else _wsl_raw(cmd, timeout)

def _wsl_raw(cmd, timeout=60):
    """Raw WSL exécution for arbitrary bash commands."""
    import subprocess
    full = ['wsl', '-d', 'Ubuntu', '--', 'bash', '-lc', cmd]
    try:
        r = subprocess.run(full, capture_output=True, text=True, timeout=timeout)
        return r.returncode, r.stdout, r.stderr
    except subprocess.TimeoutExpired:
        return -1, '', f'TIMEOUT after {timeout}s'

# Verify paths are functional
assert (WIN_LEAN_PROJECT / 'lakefile.lean').exists(), 'conway_lean/lakefile.lean not found'
print('Setup OK : Lean project detecte automatiquement (via lean_notebook_utils)')
print(f'WSL path: .../conway_lean (lettre drive: {WIN_LEAN_PROJECT.drive[0]})')
print(f'Windows path: .../conway_lean')

Setup OK : Lean project detecte automatiquement (via lean_notebook_utils)
WSL path: .../conway_lean (lettre drive: D)
Windows path: .../conway_lean

# Statistiques des modules Life
life_dir = WIN_LEAN_PROJECT / 'Conway' / 'Life'
life_files = {
    'Life.lean': life_dir.parent / 'Life.lean',
    'Life/Spaceships.lean': life_dir / 'Spaceships.lean',
    'Life/Oscillators.lean': life_dir / 'Oscillators.lean',
}

total_lines = 0
total_defs = 0
total_theorems = 0
total_sorry = 0

print('Statistiques des modules Life')
print('=' * 55)
for name, path in life_files.items():
    if not path.exists():
        print(f'  {name:<30s} NON TROUVE')
        continue
    content = path.read_text(encoding='utf-8')
    lines = content.splitlines()
    n_total = len(lines)
    n_def = sum(1 for l in lines if l.strip().startswith('def '))
    n_theorem = sum(1 for l in lines if l.strip().startswith('theorem '))
    n_sorry = content.count('sorry') - content.count('-- sorry')  # exclude comments
    print(f'  {name:<30s} {n_total:>4d} lignes | {n_def:>2d} defs | {n_theorem:>2d} thms | sorry={n_sorry}')
    total_lines += n_total
    total_defs += n_def
    total_theorems += n_theorem
    total_sorry += n_sorry

print('-' * 55)
print(f'  {"TOTAL":<30s} {total_lines:>4d} lignes | {total_defs:>2d} defs | {total_theorems:>2d} thms | sorry={total_sorry}')
print()
print(f'Cible Phase 1+2 : sorry = 0 ... {"ATTEINT" if total_sorry == 0 else "ECHEC"}')

Statistiques des modules Life
=======================================================
  Life.lean                       253 lignes | 21 defs |  8 thms | sorry=0
  Life/Spaceships.lean            139 lignes |  3 defs |  3 thms | sorry=0
  Life/Oscillators.lean           226 lignes |  7 defs |  7 thms | sorry=0
-------------------------------------------------------
  TOTAL                           618 lignes | 31 defs | 18 thms | sorry=0

Cible Phase 1+2 : sorry = 0 ... ATTEINT

Interpretation : statut Phase 1 + Phase 2

Les modules Life sont compacts (lignes non tenues en prose) mais couvrent toutes les briques fondamentales du Game of Life :

Module	Théorèmes	Patterns
Life.lean	block, beehive, blinker, toad, beacon, glider	Fondations B3/S23
Spaceships.lean	LWSS, MWSS, HWSS	Vaisseaux period-4
Oscillators.lean	loaf, boat, tub, pond, ship + pulsar p3, pentadecathlon p15	Still-lifes + oscillateurs

Aucun sorry sur les modules Life. L’ensemble lake build Conway compile avec SUCCESS. Les théorèmes “borderline” (pulsar (population 48), pentadecathlon (periode 15)) passent native_decide sans timeout.

La vérification finale s’effectue par lake build dans la section suivante.

6.1 Interroger la source de verite : #eval du zoo A4

Les sections précédentes ont illustre numeriquement (numpy) le comportement des patterns. Ici on interroge directement la source de verite Lean : les predicats isSpaceship, isStillLife et isOscillator définis dans Conway.Life, Conway.Life.Spaceships et Conway.Life.Oscillators.

Ces predicats sont des fonctions booleennes sur Grid = List (Int x Int). Ce sont exactement les mêmes définitions que celles fermees par les théorèmes native_decide du port Lean (issue A4) : un #eval p = true ici correspond a un théorème p = true := by native_decide la-bas. La cellule ci-dessous ecrit un fichier .lean qui importe les modules, évalue le zoo de patterns produit par A4, et exécute via lake env lean :

• Vaisseaux (Spaceships.lean) : LWSS, MWSS, HWSS — isSpaceship _ 4 (0, 2) (période 4, deplacement de 2 cellules).
• Still-lifes supplémentaires (Oscillators.lean) : loaf, boat, pond — isStillLife _.
• Oscillateur : pulsar (période 3) — isOscillator pulsar 3.

#eval interprete vs native_decide. Le #eval ci-dessus exerce l’interprete Lean : il convient aux predicats peu profonds (quelques generations). Le pentadecathlon, lui, demande 15 generations : son #eval interprete serait lent, alors que le théorème pentadecathlon_period_15 : isOscillator pentadecathlon 15 = true := by native_decide (section 7) compile la decision en code natif — c’est tout l’intérêt de native_decide. On laisse donc ce cas a la preuve compilee de la section 7.

Contrairement aux vérifications numpy (qui illustrent sur une grille bornee), ces #eval exercent le code formellement vérifié : si l’un retournait false, le théorème correspondant serait faux. C’est la différence entre « le notebook montre » et « Life.lean prouve ».

# Interroge la source de verite : #eval direct sur les predicats Lean réels du zoo A4.
# On ecrit un fichier .lean qui importe les modules Life et évalue chaque pattern,
# puis on l'exécute via `lake env lean`. Chaque `true` = sortie de la fonction Bool
# (les memes définitions que ferment les théorèmes `native_decide` du port Lean).
# Le chargement de l'environnement Lean (imports Mathlib) prend quelques minutes.
snippet = """import Conway.Life
import Conway.Life.Spaceships
import Conway.Life.Oscillators
open Conway.Life
-- Vaisseaux (Spaceships.lean) : période 4, deplacement (0, 2)
#eval isSpaceship lwss 4 (0, 2)
#eval isSpaceship mwss 4 (0, 2)
#eval isSpaceship hwss 4 (0, 2)
-- Still-lifes supplémentaires (Oscillators.lean)
#eval isStillLife loaf
#eval isStillLife boat
#eval isStillLife pond
-- Oscillateur pulsar : période 3, 48 cellules
#eval isOscillator pulsar 3"""

labels = [
    "isSpaceship lwss 4 (0,2)   [LWSS  -- vaisseau leger, periode 4]",
    "isSpaceship mwss 4 (0,2)   [MWSS  -- vaisseau moyen, periode 4]",
    "isSpaceship hwss 4 (0,2)   [HWSS  -- vaisseau lourd, periode 4]",
    "isStillLife loaf           [loaf  -- nature morte]",
    "isStillLife boat           [boat  -- nature morte]",
    "isStillLife pond           [pond  -- nature morte]",
    "isOscillator pulsar 3      [pulsar -- oscillateur periode 3, 48 cellules]",
]

print("#eval direct sur les predicats Lean de Life (zoo A4, source de verite unique)...")
print("Chargement de l'environnement Lean + #eval interprete (peut prendre 2-6 min)...")
print("-" * 70)
rc, out, err = wsl(
    "cat > /tmp/_nb_eval.lean <<'LEANEOF'\n" + snippet + "\nLEANEOF\n"
    f"source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && lake env lean /tmp/_nb_eval.lean 2>&1; rm -f /tmp/_nb_eval.lean",
    timeout=900,
)
# Parsing robuste : lignes finissant par 'true'/'false' (avec ou sans prefixe file:line:col:)
results = [l.rstrip().split()[-1] for l in out.splitlines()
           if l.rstrip().endswith(("true", "false"))]

if len(results) == len(labels):
    n_true = sum(1 for r in results if r == "true")
    for lbl, r in zip(labels, results):
        mark = "OK" if r == "true" else "!!"
        print(f"  [{mark}] {lbl} -> {r}")
    print("-" * 70)
    print(f"  {n_true}/{len(labels)} predicats du zoo A4 evalues a `true`")
    print("  (memes definitions Bool que les theoremes prouves par native_decide).")
    print("  Note : pentadecathlon (periode 15) est prouve par native_decide en")
    print("  section 7 ; le #eval interprete serait lent sur 15 generations, alors")
    print("  que native_decide compile la decision (rapide a la preuve).")
else:
    # Sortie inattendue : afficher le brut pour diagnostic (jamais de verdict creux)
    print("Sortie brute de lake env lean (parse incomplet) :")
    print(out if out.strip() else "(aucune sortie)")
    print(f"  (rc={rc}, {len(results)} verdicts true/false parses sur {len(labels)} attendus)")
    if err and err.strip() and "TIMEOUT" not in err:
        print("STDERR:", err[-300:])

#eval direct sur les predicats Lean de Life (zoo A4, source de verite unique)...
Chargement de l'environnement Lean + #eval interprete (peut prendre 2-6 min)...
----------------------------------------------------------------------
  [OK] isSpaceship lwss 4 (0,2)   [LWSS  -- vaisseau leger, periode 4] -> true
  [OK] isSpaceship mwss 4 (0,2)   [MWSS  -- vaisseau moyen, periode 4] -> true
  [OK] isSpaceship hwss 4 (0,2)   [HWSS  -- vaisseau lourd, periode 4] -> true
  [OK] isStillLife loaf           [loaf  -- nature morte] -> true
  [OK] isStillLife boat           [boat  -- nature morte] -> true
  [OK] isStillLife pond           [pond  -- nature morte] -> true
  [OK] isOscillator pulsar 3      [pulsar -- oscillateur periode 3, 48 cellules] -> true
----------------------------------------------------------------------
  7/7 predicats du zoo A4 evalues a `true`
  (memes definitions Bool que les theoremes prouves par native_decide).
  Note : pentadecathlon (periode 15) est prouve par native_decide en
  section 7 ; le #eval interprete serait lent sur 15 generations, alors
  que native_decide compile la decision (rapide a la preuve).

Exercice 4 : faites vérifier un still-life par Lean

Vous venez de voir (6.1) comment #eval isStillLife loaf interroge directement la source de verite Life.lean. A votre tour : choisissez un still-life — ou inventez des coordonnees — et demandez a Lean de trancher, formellement.

A vous : completez coords avec les cellules d’un still-life de votre choix (le block : [(0,0), (0,1), (1,0), (1,1)], ou essayez le tub, le boat…). La cellule lance alors #eval isStillLife <vos coords> dans le vrai projet Lean via lake env lean. Si Lean repond true, votre pattern est formellement un still-life ; sinon, ce n’en est pas un. C’est vous qui pilotez la source de verite.

# TODO étudiant : remplacez None par les coordonnees d'un still-life de VOTRE choix.
# Format Lean d'une Grid = liste de paires d'entiers.
#   Exemple (block 2x2) : "[(0, 0), (0, 1), (1, 0), (1, 1)]"
#   Indice : un still-life vérifie step(g) == g ; block, beehive, tub, pond en sont.
coords = None  # TODO étudiant : ex. "[(0, 0), (0, 1), (1, 0), (1, 1)]"

if coords is None:
    print("Exercice 4 a completer : definissez `coords` (liste de cellules au format Lean) ci-dessus.")
else:
    snippet = f"""import Conway.Life
open Conway.Life
#eval isStillLife {coords}"""
    rc, out, err = wsl(
        "cat > /tmp/_ex3_eval.lean <<'LEANEOF'\n" + snippet + "\nLEANEOF\n"
        f"source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && lake env lean /tmp/_ex3_eval.lean 2>&1; rm -f /tmp/_ex3_eval.lean",
        timeout=300
    )
    verdicts = [l.rstrip().split()[-1] for l in out.splitlines()
                if l.rstrip().endswith(('true', 'false'))]
    print(f"Lean : #eval isStillLife {coords}")
    print(out.strip() or "(pas de sortie)")
    if verdicts:
        val = verdicts[-1]
        print(f"=> Verdict Lean : {val} ({'still-life confirme par la source de verite !' if val == 'true' else 'PAS un still-life'})")

Exercice 4 a completer : definissez `coords` (liste de cellules au format Lean) ci-dessus.

6.2 Le parseur RLE prouve : #eval parseRLE (source de verite vs re-implémentation Python)

A la section 3, pour afficher les trois piliers, nous avons parse leurs fichiers RLE avec une petite fonction Python (parse_rle). C’est commode pour la visualisation matplotlib, mais ce n’est qu’une illustration : rien ne garantit que ce parseur Python soit correct.

Le port Lean, lui, fournit un parseur RLE entierement prouve : Conway.Life.RLE.parseRLE : String -> Except String Grid (fichier conway_lean/Conway/Life/RLE.lean, sans sorry). Mieux : le module accompagne le parseur de théorèmes de correction fermes par native_decide :

• glider_parse_ok, lwss_parse_ok, pulsar_parse_ok, gosper_gun_parse_ok : les RLE phares parsent sans erreur.
• lwss_rle_roundtrip : lwss_parsed = lwss et pulsar_rle_roundtrip : pulsar_parsed = pulsar : le Grid produit par parseRLE est exactement egal a la constante ecrite a la main dans Conway.Life — un round-trip prouve, pas une coincidence observee a l’oeil.
• gosper_gun_cell_count : gosper_gun.length = 36 : le canon de Gosper a exactement 36 cellules.

La cellule ci-dessous interroge directement cette source de verite : on #eval le vrai parseRLE sur les chaînes RLE des patterns (glider, LWSS, pulsar, canon de Gosper) et on retrouve les comptes de cellules attendus (5, 9, 48, 36) ainsi que l’égalité round-trip. C’est la différence entre « le notebook parse en Python pour dessiner » et « Lean parse et prouve que le parse est correct ».

# Source de verite : #eval du PARSEUR RLE PROUVÉ de Lean (Conway.Life.RLE.parseRLE).
# Contraste avec le `parse_rle` Python de la section 3 (qui n'illustre que pour matplotlib) :
# ici parseRLE est entierement prouvé (0 sorry) et accompagne de théorèmes native_decide
# (glider/lwss/pulsar/gosper_gun_parse_ok, lwss/pulsar_rle_roundtrip, gosper_gun_cell_count).
snippet = """import Conway.Life.RLE
open Conway.Life Conway.Life.RLE
-- parseRLE : String -> Except String Grid (entierement prouvé, 0 sorry, RLE.lean)
#eval (parseRLE glider_RLE).toOption.isSome   -- le glider parse sans erreur
#eval glider_parsed.length                     -- 5 cellules vivantes
#eval lwss_parsed.length                        -- 9 cellules (LWSS)
#eval pulsar_parsed.length                      -- 48 cellules (pulsar)
#eval gosper_gun.length                         -- 36 cellules (canon de Gosper)
#eval (lwss_parsed == lwss)                     -- round-trip : == la constante lwss
#eval (pulsar_parsed == pulsar)"""

labels = [
    ("(parseRLE glider_RLE).toOption.isSome", "true", "le glider RLE parse sans erreur (glider_parse_ok)"),
    ("glider_parsed.length",                  "5",    "Grid du glider : 5 cellules vivantes"),
    ("lwss_parsed.length",                    "9",    "Grid du LWSS : 9 cellules"),
    ("pulsar_parsed.length",                  "48",   "Grid du pulsar : 48 cellules"),
    ("gosper_gun.length",                     "36",   "Grid du canon de Gosper : 36 cellules"),
    ("lwss_parsed == lwss",                   "true", "round-trip prouve : parseRLE == constante lwss (lwss_rle_roundtrip)"),
    ("pulsar_parsed == pulsar",               "true", "round-trip prouve : parseRLE == constante pulsar (pulsar_rle_roundtrip)"),
]

import re
print("#eval du parseur RLE PROUVE de Lean (Conway.Life.RLE.parseRLE, 0 sorry)...")
print("Chargement de l'environnement Lean + #eval interprete (peut prendre 2-6 min)...")
print("-" * 70)
rc, out, err = wsl(
    "cat > /tmp/_nb_rle.lean <<'LEANEOF'\n" + snippet + "\nLEANEOF\n"
    f"source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && lake env lean /tmp/_nb_rle.lean 2>&1; rm -f /tmp/_nb_rle.lean",
    timeout=900,
)
# Parsing robuste : lignes qui sont exactement un résultat #eval (entier ou true/false)
RES = re.compile(r"^(true|false|\d+)$")
results = [l.strip() for l in out.splitlines() if RES.match(l.strip())]

if len(results) == len(labels):
    n_ok = 0
    for (expr, expected, desc), got in zip(labels, results):
        ok = (got == expected)
        n_ok += ok
        mark = "OK" if ok else "!!"
        print(f"  [{mark}] {expr} -> {got}   ({desc})")
    print("-" * 70)
    print(f"  {n_ok}/{len(labels)} #eval du parseur RLE conformes aux valeurs attendues.")
    print("  parseRLE est entierement prouve (0 sorry) ; les round-trips lwss/pulsar sont")
    print("  fermes par native_decide. Le `parse_rle` Python de la section 3 n'est qu'une")
    print("  illustration pour matplotlib : ici, Lean *prouve* la correction du parse.")
else:
    print("Sortie brute de lake env lean (parse incomplet) :")
    print(out if out.strip() else "(aucune sortie)")
    print(f"  (rc={rc}, {len(results)} verdicts parses sur {len(labels)} attendus)")
    if err and err.strip() and "TIMEOUT" not in err:
        print("STDERR:", err[-300:])

#eval du parseur RLE PROUVE de Lean (Conway.Life.RLE.parseRLE, 0 sorry)...
Chargement de l'environnement Lean + #eval interprete (peut prendre 2-6 min)...
----------------------------------------------------------------------
  [OK] (parseRLE glider_RLE).toOption.isSome -> true   (le glider RLE parse sans erreur (glider_parse_ok))
  [OK] glider_parsed.length -> 5   (Grid du glider : 5 cellules vivantes)
  [OK] lwss_parsed.length -> 9   (Grid du LWSS : 9 cellules)
  [OK] pulsar_parsed.length -> 48   (Grid du pulsar : 48 cellules)
  [OK] gosper_gun.length -> 36   (Grid du canon de Gosper : 36 cellules)
  [OK] lwss_parsed == lwss -> true   (round-trip prouve : parseRLE == constante lwss (lwss_rle_roundtrip))
  [OK] pulsar_parsed == pulsar -> true   (round-trip prouve : parseRLE == constante pulsar (pulsar_rle_roundtrip))
----------------------------------------------------------------------
  7/7 #eval du parseur RLE conformes aux valeurs attendues.
  parseRLE est entierement prouve (0 sorry) ; les round-trips lwss/pulsar sont
  fermes par native_decide. Le `parse_rle` Python de la section 3 n'est qu'une
  illustration pour matplotlib : ici, Lean *prouve* la correction du parse.

7. Vérification : lake build des modules Life

On vérifie que la fondation Life — Conway/Life.lean + Conway/Life/Spaceships.lean + Conway/Life/Oscillators.lean, la source de verite unique de ce notebook — compile avec SUCCESS (exit code 0), puis on compte les sorrys de maniere honnete (cellule suivante).

On cible explicitement les modules Life (lake build Conway.Life Conway.Life.Spaceships Conway.Life.Oscillators) plutot que le Conway complet : cela concentre la vérification sur ce que le notebook met en avant. Les modules Phase 3b (Hashlife) ont leurs propres sorries de roadmap, traces en Annexe G et hors-scope ici.

Note : le build de Mathlib peut prendre plusieurs minutes au premier lancement (cache cold). Pour cette exécution Papermill, on utilise un timeout large (1500s).

import subprocess

# On build EXPLICITEMENT les modules Life = la source de verite unique du notebook.
# (Build cible plutot que `lake build Conway` complet : focus sur la fondation Life,
#  les modules Hashlife/Phase-3b avec leurs sorries de roadmap restent hors-scope ici.)
targets = 'Conway.Life Conway.Life.Spaceships Conway.Life.Oscillators'
print(f'Lancement de lake build des modules Life ... (timeout 1500s)')
print(f'  cible : {targets}')
print('-' * 60)

try:
    rc, out, err = wsl(
        f'source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && lake build {targets} 2>&1 | tail -20',
        timeout=1500
    )
    print(out)
    if err and err.strip() and not err.strip().startswith('TIMEOUT'):
        print('STDERR:', err[-300:])
    print()
    print(f'Exit code : {rc}')
    if rc == 0:
        print('SUCCESS : les 3 modules Life compilent (fondation single-source-of-truth, 0 sorry).')
    elif rc == -1:
        print('TIMEOUT : la verification CI / build local du PR est autoritative.')
    else:
        print('ECHEC : voir log ci-dessus.')
except Exception as e:
    print(f'Exception : {e}')

Lancement de lake build des modules Life ... (timeout 1500s)
  cible : Conway.Life Conway.Life.Spaceships Conway.Life.Oscillators
------------------------------------------------------------
info: Conway/Life/Spaceships.lean:67:0: [(0, 3), (0, 4), (0, 5), (0, 6), (1, 2), (1, 6), (2, 6), (3, 2), (3, 5)]
info: Conway/Life/Spaceships.lean:68:0: [(0, 3), (0, 4), (0, 5), (0, 6), (1, 2), (1, 6), (2, 6), (3, 2), (3, 5)]
info: Conway/Life/Spaceships.lean:69:0: true
info: Conway/Life/Spaceships.lean:98:0: [(0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (1, 0), (1, 5), (2, 5), (3, 0), (3, 4), (4, 2)]
info: Conway/Life/Spaceships.lean:99:0: [(0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (1, 2), (1, 7), (2, 7), (3, 2), (3, 6), (4, 4)]
info: Conway/Life/Spaceships.lean:100:0: [(0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (1, 2), (1, 7), (2, 7), (3, 2), (3, 6), (4, 4)]
info: Conway/Life/Spaceships.lean:101:0: true
info: Conway/Life/Spaceships.lean:130:0: [(0, 1), (0, 2), (0, 3), (0, 4), (0, 5), (0, 6), (1, 0), (1, 6), (2, 6), (3, 0), (3, 5), (4, 2), (4, 3)]
info: Conway/Life/Spaceships.lean:131:0: [(0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (0, 8), (1, 2), (1, 8), (2, 8), (3, 2), (3, 7), (4, 4), (4, 5)]
info: Conway/Life/Spaceships.lean:132:0: [(0, 3), (0, 4), (0, 5), (0, 6), (0, 7), (0, 8), (1, 2), (1, 8), (2, 8), (3, 2), (3, 7), (4, 4), (4, 5)]
info: Conway/Life/Spaceships.lean:133:0: true
ℹ [3008/3008] Replayed Conway.Life.Oscillators
info: Conway/Life/Oscillators.lean:117:0: true
info: Conway/Life/Oscillators.lean:118:0: true
info: Conway/Life/Oscillators.lean:119:0: true
info: Conway/Life/Oscillators.lean:120:0: true
info: Conway/Life/Oscillators.lean:121:0: true
info: Conway/Life/Oscillators.lean:188:0: true
info: Conway/Life/Oscillators.lean:220:0: true
Build completed successfully (3008 jobs).


Exit code : 0
SUCCESS : les 3 modules Life compilent (fondation single-source-of-truth, 0 sorry).

# Vérification du nombre de sorrys RÉELS dans les 3 modules Life (source de verite unique)
life_modules = [
    'Conway/Life.lean',
    'Conway/Life/Spaceships.lean',
    'Conway/Life/Oscillators.lean',
]

print('Verification sorry — modules Life (fondation single-source) :')
print('-' * 60)
total_sorry = 0
for f in life_modules:
    rc, out, err = wsl(f'cd {LEAN_PROJECT} && grep -c sorry {f}', timeout=10)
    # grep -c : rc=0 si >=1 match, rc=1 si 0 match. out = compte.
    count = int(out.strip()) if out.strip().lstrip('-').isdigit() else 0
    print(f'  {f:<38s} sorry = {count}')
    total_sorry += count
print('-' * 60)
print(f'  Total sorry (3 modules Life) : {total_sorry}')
print(f'  Cible 0 sorry sur la fondation Life ... {"ATTEINT" if total_sorry == 0 else "ECHEC"}')
print()

# Note d'honnetete : `grep sorry Conway.lean` (le module racine) renvoie une occurrence,
# mais ce N'EST PAS une preuve manquante — c'est un COMMENTAIRE de documentation.
rc, line, err = wsl(f"cd {LEAN_PROJECT} && grep -n sorry Conway.lean", timeout=10)
print('Faux positif documente — root Conway.lean :')
for l in line.splitlines():
    print(f'   {l.strip()}')
print('   => occurrence dans un COMMENTAIRE (pas un `:= by sorry`). La fondation Life est a 0 sorry.')
print('   Les modules Hashlife (Phase 3b) ont leurs propres sorries de roadmap documentes,')
print('   hors-scope de la fondation Life couverte par ce notebook (cf Annexe G).')

Verification sorry — modules Life (fondation single-source) :
------------------------------------------------------------
  Conway/Life.lean                       sorry = 0
  Conway/Life/Spaceships.lean            sorry = 0
  Conway/Life/Oscillators.lean           sorry = 0
------------------------------------------------------------
  Total sorry (3 modules Life) : 0
  Cible 0 sorry sur la fondation Life ... ATTEINT

Faux positif documente — root Conway.lean :
   16:servent de gradient de difficulté pour le prouveur multi-agent (sorry
   57:fécond et créatif. Tous les `sorry` ne sont pas comblés — la plupart sont
   => occurrence dans un COMMENTAIRE (pas un `:= by sorry`). La fondation Life est a 0 sorry.
   Les modules Hashlife (Phase 3b) ont leurs propres sorries de roadmap documentes,
   hors-scope de la fondation Life couverte par ce notebook (cf Annexe G).

8. Conclusion

Ce notebook clot la Phase 0 de l’Epic #1647 et accompagne les phases 1+5 mergees (Life.lean + Spaceships.lean + Oscillators.lean). Resume de la livraison :

Élément	Statut	Detail
Notebook Lean-16b-Conway-Game-of-Life-Lean.ipynb	LIVRE	demo Python, statistiques Lean, feuille de route
Module Conway/Life.lean	LIVRE	théorèmes prouves, sans sorry
Module Conway/Life/Spaceships.lean	LIVRE (PR #1975)	théorèmes (LWSS/MWSS/HWSS), sans sorry
Module Conway/Life/Oscillators.lean	LIVRE (PR #1975)	théorèmes (still-lifes + pulsar + pentadecathlon), sans sorry
lake build Conway	SUCCESS	sans sorry
Roadmap Phases 2-9	TRACEE	Hashlife en cours (Phases 3a/3b)

Total provable : tous les théorèmes des modules Life, sans sorry.

Le prochain jalon clef est Hashlife (Phases 3a+3b) : une fois le quadtree MacroCell et le step récursif implantes et prouves corrects, les 3 piliers communautaires (OTCA, CPU, Gemini) deviennent accessibles via le facteur de compression exponentiel.

L’histoire en trois actes, et ce qu’il reste a prouver

Ce notebook a raconte une montee en puissance : une cellule qui se reflete (OTCA Metapixel), une grille qui calcule (la machine de Rendell, puis le CPU de Carlini), un motif qui se reproduit (Gemini). Cette progression - emulation, calcul, reproduction - n’est pas qu’une jolie narration : c’est exactement la feuille de route formelle de l’Epic #1647. Chaque acte attend son native_decide (otca_self_emulates, spartan_adder_correct, gemini_replicates), et tous reposent sur le même verrou technique, la correction de Hashlife (Phases 3a/3b), sans laquelle aucun temoin a \(10^7\) generations n’est decidable. Porter ces théorèmes, c’est transformer la belle histoire de la communaute Life en certificat vérifié par machine.

Reconnaissances

• John H. Conway (1937-2020) : pour le Game of Life et tout le reste
• Andrew J. Wade : pour Gemini (2010)
• Brice Due : pour OTCA Metapixel (2006)
• Nicholas Carlini : pour le 8-bit computer (2020)
• Adam P. Goucher : pour le Spartan adder et les pillars de l’analyse de patterns
• Paul Rendell : pour la machine de Turing dans Life (2000)
• Bill Gosper : pour hashlife (1984)
• La communaute LifeWiki qui maintient le catalogue

Lectures complementaires

1. Conway, Berlekamp, Guy, Winning Ways for Your Mathematical Plays vol. 2, 1982. Chapitre Life.
2. Rendell, Turing Machine Universality of the Game of Life, Springer (Emergence, Complexity and Computation), 2016.
3. LifeWiki : conwaylife.com/wiki/ - catalogue communautaire complet.
4. Gonthier, Formal proof - the four-color theorem, Notices of the AMS, 2008. Modèle de preuve par reflexion.

---

Navigation : << Lean-15 Grothendieck | Index | Lean-16c Compagnon Golly >>

Annexes — approfondissements optionnels

La lecture simple s’arrête à la conclusion. Les annexes regroupent les approfondissements, sans aucune suppression de contenu : le rappel des noix Phase 1 (A), la logique constructive Spartan (B), l’intuition Hashlife (C), le port Lean en détail (D), la limite des string literals (E), le scaffold Pillars.lean (F) et la feuille de route de l’Epic #1647 (G). Chaque annexe est autonome et préserve l’intégralité du texte des sections d’origine.

Annexe A — Rappel Phase 1 : les noix de Conway déjà portees

L’Epic #1151 (Phase 1, mergee mai 2026) a porte en Lean 4 des résultats moins celebres mais élégants de John Conway. Tous vivent dans conway_lean/Conway/, sans sorry de production. Voici un rapide #check de chacun.

Module	Résultat	Théorème phare
Conway.Doomsday	Algorithme du Doomsday	dayOfWeek 2020 4 11 = saturday (Conway est mort un samedi)
Conway.LookAndSay	Suite audioactive	lookAndSay [1] = [1,1] etc. (Cosmological theorem deferred)
Conway.Fractran	Machine de Turing programmable	fractran_step correctness
Conway.Nim	Sprague-Grundy	isWinningNim [3,4,5] = true
Conway.Angel	Problème de l’ange	(angelMoves 1).card = 8 (king moves)

Vérification en sub-process Lean : on appelle lean --search pour confirmer que les définitions existent dans le module Conway.

# Lister les fichiers Phase 1 + Phase 2 du module Conway
modules = sorted([p.name for p in (WIN_LEAN_PROJECT / 'Conway').glob('*.lean')])
life_modules = sorted([p.name for p in (WIN_LEAN_PROJECT / 'Conway' / 'Life').glob('*.lean')])

print('Modules dans conway_lean/Conway/ :')
for m in modules:
    path = WIN_LEAN_PROJECT / 'Conway' / m
    lines = len(path.read_text(encoding='utf-8').splitlines())
    print(f'  {m:<30s} {lines:>5d} lignes')
print()
print('Modules dans conway_lean/Conway/Life/ :')
for m in life_modules:
    path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / m
    lines = len(path.read_text(encoding='utf-8').splitlines())
    print(f'  {m:<30s} {lines:>5d} lignes')

Modules dans conway_lean/Conway/ :
  Angel.lean                       152 lignes
  Angel_en.lean                    149 lignes
  CHSH.lean                         88 lignes
  CHSHLandau.lean                  283 lignes
  CHSHLandau_en.lean               283 lignes
  CHSHQuantum.lean                 167 lignes
  CHSHQuantum_en.lean              166 lignes
  CHSHRandomized.lean              176 lignes
  CHSHRandomized_en.lean           177 lignes
  CHSH_en.lean                      90 lignes
  CollatzLike.lean                 274 lignes
  CollatzLike_en.lean              202 lignes
  Doomsday.lean                    163 lignes
  DoomsdayLemmas.lean               52 lignes
  DoomsdayLemmas_en.lean            54 lignes
  Doomsday_en.lean                 123 lignes
  Fractran.lean                     74 lignes
  FractranLemmas.lean               74 lignes
  FractranLemmas_en.lean            75 lignes
  Fractran_en.lean                  75 lignes
  FreeWillTheorem.lean             221 lignes
  FreeWillTheorem_en.lean          236 lignes
  KochenSpecker.lean               357 lignes
  KochenSpecker_en.lean            270 lignes
  Life.lean                        253 lignes
  Life_en.lean                     246 lignes
  LookAndSay.lean                   90 lignes
  LookAndSayLemmas.lean             62 lignes
  LookAndSayLemmas_en.lean          63 lignes
  LookAndSay_en.lean                82 lignes
  MathlibMap.lean                  120 lignes
  MathlibMap_en.lean               183 lignes
  Nim.lean                         156 lignes
  Nim_en.lean                      147 lignes

Modules dans conway_lean/Conway/Life/ :
  AdversarialBattery.lean          213 lignes
  AdversarialBatteryG2.lean        154 lignes
  AdversarialBatteryG2_en.lean     157 lignes
  AdversarialBattery_en.lean       217 lignes
  Computation.lean                 314 lignes
  Computation_en.lean              309 lignes
  ConeGeometry.lean                314 lignes
  ConeGeometry_en.lean             217 lignes
  DecideProbe.lean                 125 lignes
  DecideProbe_en.lean              131 lignes
  GridCanonical.lean               505 lignes
  GridCanonical_en.lean            363 lignes
  Hashlife.lean                    973 lignes
  HashlifeCorrectness.lean        7441 lignes
  HashlifeMarginDemo.lean          100 lignes
  HashlifeMarginDemo_en.lean        98 lignes
  HashlifeMarginFragment.lean     1985 lignes
  HashlifeMarginFragment_en.lean  1986 lignes
  HashlifeMemo.lean                360 lignes
  HashlifeMemo_en.lean             356 lignes
  Hashlife_en.lean                 961 lignes
  JumpCapture.lean                 608 lignes
  LightCone.lean                   626 lignes
  LightCone_en.lean                473 lignes
  MacroCell.lean                   912 lignes
  MacroCell_en.lean                888 lignes
  Novelty.lean                     269 lignes
  Novelty_en.lean                  268 lignes
  Oscillators.lean                 226 lignes
  Oscillators_en.lean              223 lignes
  PatternTour.lean                 199 lignes
  PatternTour_en.lean              195 lignes
  Pillars.lean                     246 lignes
  Pillars_en.lean                  234 lignes
  RLE.lean                         366 lignes
  RLE_en.lean                      357 lignes
  Spaceships.lean                  139 lignes
  Spaceships_en.lean               138 lignes

Interpretation : modules Conway en Lean 4

Les modules Phase 1 (Doomsday, LookAndSay, Fractran, Nim, Angel) + les modules de lemmes (DoomsdayLemmas, LookAndSayLemmas) + le nouveau Life.lean que nous introduisons dans ce notebook. KochenSpecker.lean est un module distinct (Pilier 1 de l’Epic #1651, Conway Free Will Theorem) — desormais sans sorry (PR #2019, argument de parite). FreeWillTheorem.lean (PR #2026) complète le théorème de libre arbitre, sans sorry.

Statut sorry : aucun sur Doomsday/LookAndSay/Fractran/Nim/Angel/Life/KochenSpecker/FreeWillTheorem. Une cible globale lake build Conway compile avec SUCCESS.

Annexe B — Spartan logic + flux de gliders = logique constructive

Le pari de l’Epic #1647 est qu’on peut prouver formellement la calculabilite universelle du Game of Life par un argument de construction. L’argument moderne (Wade 2010, Goucher 2014) procede en trois étages :

1. Spartan logic : on isole des configurations statiques (still lifes ou patterns stables) qui jouent le rôle de “transistors” ou “portes logiques”. Le gating - decider si un signal passe ou non - se fait par presence ou absence d’un still life a un endroit donné.

2. Glider streams : les signaux sont transportes par des flux de gliders, periodiques et orientes. Un glider stream represente un bit (la cellule est presente ou absente a un instant fixe modulo la période).

3. Composition : la composition d’une porte NAND universelle suffit pour realiser tout calcul booléen, donc tout calcul Turing (théorème classique).

L’analogie ribosome / ARN du mandat utilisateur (mai 2026) :

“logique constructive spartian pour le ribosome, et flux de gliders pour le brin d’ARN”

Le ribosome = la machine fixe qui lit l’instruction ; en Life, c’est le sous-circuit Spartan. Le brin d’ARN = la sequence d’instructions, ici un flux de gliders periodique. La construction de Gemini (section 3) suit exactement ce paradigme : un ribosome stationnaire interprete un flux de gliders qui construit une copie de lui-même un peu plus loin.

Cette periodicite spatio-temporelle forte est ce qui rend hashlife efficace sur Gemini.

Annexe C — Intuition Hashlife (Gosper 1984)

Le problème de tractabilite des piliers communautaires : Gemini fait 33 699 586 generations pour se repliquer une fois. Une simulation cellule-par-cellule O(N x T) ou N ~ 10^5 et T ~ 10^7 demande 10^12 opérations - intractable.

Hashlife (Bill Gosper, Symbolics 1984) exploite deux observations :

1. Periodicite spatio-temporelle : les patterns de Life sont massivement repetitifs. Un still life ne change pas ; un blinker repete chaque 2 generations ; un glider stream est periodique en temps comme en espace.

2. Macrocells : on encode l’univers sous forme arborescente :

   • Niveau 0 : cellule unique
   • Niveau 1 : la grille 2x2
   • Niveau n+1 : 4 macrocells de niveau n (un nord-ouest, nord-est, sud-ouest, sud-est)

Avec canonicalisation par hash : deux macrocells identiques en mémoire ne sont stockees qu’une seule fois.

Step récursif et compression exponentielle

Un macrocell de niveau \(n\) couvre une zone \(2^n \times 2^n\). Hashlife calcule l’évolution du centre \(2^{n-1} \times 2^{n-1}\) après \(2^{n-2}\) generations en un seul appel récursif memoise. La memoization sur les hashes fait que le nombre d’appels distincts est borne par la diversite spatiale du pattern, pas par \(T\).

Pour un pattern hautement periodique (comme Gemini), la diversite spatiale est polylog(T) - donc le step “fast-forward” de \(2^k\) generations devient effectivement \(O(k)\) après warmup, factor de compression exponentiel.

Théorème central de correction

Une fois hashlife implemente en Lean (Phase 3 de l’Epic #1647), il faut prouver la correction :

theorem hashlife_correct : forall n mc,
  expand (hashlife_step mc) = step^[2^n] (center_region (expand mc))

Cette preuve est l’invariant central de l’Epic : tout le reste (Gemini, OTCA, Beluchenko CPU digital) en derive par native_decide sur des temoins concrets. La preuve elle-même se fait par induction sur le niveau \(n\) + analyse de cas du step central 4x4 (decide pour \(n = 2\), induction pour \(n + 1\)).

Annexe D — Le port Lean 4 en détail : conway_lean/Conway/Life.lean

Le fichier conway_lean/Conway/Life.lean est la Phase 1 de l’Epic #1647 : les fondations Lean du Game of Life. Cible : sans sorry, lake build Conway.Life SUCCESS local.

D.1 Encodage : List (Int × Int) et non Finset

Le choix crucial de la representation a ete guide par la compatibilite avec native_decide :

abbrev Grid := List (Int × Int)

Pourquoi List plutot que Finset (Int × Int) ? L’égalité Finset fait intervenir Quot.lift (le type est un quotient de listes par permutation). Quand le kernel Lean essaie de reduire Finset equality construit via image/biUnion/filter, il doit traverser cette couche de quotients — ca explose le budget de reduction.

En revanche, l’égalité de List est une comparaison structurelle (cons par cons). En stockant les cellules dans l’ordre lexicographique trie, le step produit une liste dans le même ordre, et native_decide vérifie true/false en un éclair.

D.2 Le step B3/S23 sur List

def mooreNeighbors (p : Int × Int) : List (Int × Int) := ...
def isAlive (g : Grid) (p : Int × Int) : Bool := g.elem p
def liveNeighborCount (g : Grid) (p : Int × Int) : Nat :=
  (mooreNeighbors p).countP (isAlive g)
def aliveNext (g : Grid) (p : Int × Int) : Bool :=
  let n := liveNeighborCount g p
  if isAlive g p then (n == 2 || n == 3) else (n == 3)
def sortDedup (l : List (Int × Int)) : List (Int × Int) :=
  (l.mergeSort (fun a b => lexLt a b = true)).eraseDups
def step (g : Grid) : Grid :=
  sortDedup ((candidates g).filter (fun p => aliveNext g p))
def evolve (n : Nat) (g : Grid) : Grid := step^[n] g

Note cle : tous les predicats retournent Bool, pas Prop. Cela permet a native_decide de compiler vers du code natif et de vérifier par exécution directe.

D.3 Predicats (Bool-valued pour native_decide)

def isStillLife (g : Grid) : Bool := step g == g
def isOscillator (g : Grid) (n : Nat) : Bool := evolve n g == g
def isSpaceship (g : Grid) (n : Nat) (v : Int × Int) : Bool :=
  evolve n g == shift v g

Les trois retournent Bool et sont utilisables directement avec native_decide pour prouver ... = true.

D.4 Patterns canoniques (Phase 1)

def block : Grid := [(0, 0), (0, 1), (1, 0), (1, 1)]
def blinker_h : Grid := [(0, 0), (1, 0), (2, 0)]
def glider : Grid := [(0, 0), (1, 0), (1, 2), (2, 0), (2, 1)]
-- + beehive, blinker_v, toad, beacon

D.5 Microproofs Phase 1

theorem block_still_life : isStillLife block = true := by native_decide
theorem beehive_still_life : isStillLife beehive = true := by native_decide
theorem blinker_period_two : isOscillator blinker_h 2 = true := by native_decide
theorem toad_period_two : isOscillator toad 2 = true := by native_decide
theorem beacon_period_two : isOscillator beacon 2 = true := by native_decide
theorem glider_spaceship : isSpaceship glider 4 (1, -1) = true := by native_decide

D.6 Phase 2 : Spaceships + Oscillateurs (PR #1975)

De nouveaux modules etendent les fondations :

Conway/Life/Spaceships.lean — vaisseaux period-4, displacement (0, 2) :

theorem lwss_spaceship : isSpaceship lwss 4 (0, 2) = true := by native_decide
theorem mwss_spaceship : isSpaceship mwss 4 (0, 2) = true := by native_decide
theorem hwss_spaceship : isSpaceship hwss 4 (0, 2) = true := by native_decide

Conway/Life/Oscillators.lean — still-lifes supplémentaires + oscillateurs majeurs :

-- still-lifes supplémentaires
theorem loaf_still_life : isStillLife loaf = true := by native_decide
theorem boat_still_life : isStillLife boat = true := by native_decide
theorem tub_still_life : isStillLife tub = true := by native_decide
theorem pond_still_life : isStillLife pond = true := by native_decide
theorem ship_still_life : isStillLife ship = true := by native_decide
-- oscillateurs "borderline" qui passent native_decide !
theorem pulsar_period_three : isOscillator pulsar 3 = true := by native_decide
theorem pentadecathlon_period_15 : isOscillator pentadecathlon 15 = true := by native_decide

Total : tous les théorèmes prouves, sans sorry sur les modules Life (Life.lean + Spaceships.lean + Oscillators.lean).

Verifions les statistiques.

Annexe E — Pourquoi les piliers ne sont pas dans Lean : la limite des string literals

Le parseur RLE Lean (parseRLE) est entierement prouvé et fonctionne parfaitement sur les patterns de taille moderee (glider : population 5, pulsar : population 48, canon de Gosper : population 36). Mais les RLE des piliers communautaires sont d’un tout autre ordre de grandeur : l’OTCA Metapixel pese ~70 KB, Gemini plusieurs megaoctets.

Un string literal Lean 4 est pratique pour les patterns jusqu’a ~65 KB environ. Au-dela, le compilateur devient extremement lent ou echoue. C’est pourquoi Pillars.lean utilise des placeholders vides (([] : Grid)) pour les Initial et Target des temoins, accompagnes d’un sorry roadmap documentant le plan de chargement futur (fichier externe ou generation de code).

La cellule ci-dessous telecharge les 3 RLE et mesure leur taille pour confirmer empiriquement cette limitation. Le parseur Python parse_rle (section 3) les traite sans problème et fournit les populations et bounding boxes, servant de visualisation complementaire en attendant que le pipeline Lean puisse les accueillir.

# Pourquoi les piliers ne sont pas dans Lean : demonstration par la taille.
# Le parseur RLE Lean (Conway.Life.RLE.parseRLE) est entierement prouvé (0 sorry),
# mais il ne peut pas traiter les RLE des 3 piliers car ils sont beaucoup trop
# volumineux pour un string literal Lean. Verifions-le empiriquement.
import sys

pillar_files = {
    "OTCA Metapixel (Due 2006)": "otcametapixel.rle",
    "Machine de Turing (Rendell 2000)": "turingmachine.rle",
    "Gemini (Wade 2010)": "gemini.rle",
}

# Limites pratiques d'un string literal Lean 4 (estimation conservatrice)
LEAN_STRING_LIMIT = 65_536  # octets — au-dela, le compilateur est tres lent

print("Analyse de la taille des RLE des 3 piliers")
print("=" * 60)
print(f"Limite pratique string literal Lean 4 : ~{LEAN_STRING_LIMIT:,} octets")
print()

total_ok = 0
for label, filename in pillar_files.items():
    txt = fetch_rle(filename)
    if txt is None:
        print(f"  {label}")
        print(f"    fichier : {filename}")
        print(f"    indisponible (reseau)")
        print()
        continue
    size_bytes = len(txt.encode("utf-8"))
    W, H, xs, ys, comments = parse_rle(txt)
    population = len(xs)
    fits = "OUI" if size_bytes <= LEAN_STRING_LIMIT else "NON"
    total_ok += (size_bytes <= LEAN_STRING_LIMIT)
    ratio = size_bytes / LEAN_STRING_LIMIT
    print(f"  {label}")
    print(f"    fichier : {filename}")
    print(f"    taille : {size_bytes:,} octets ({ratio:.1f}x la limite)")
    print(f"    en-tete : {W} x {H}")
    print(f"    population : {population:,} cellules")
    print(f"    tiendrait dans un string Lean ? {fits}")
    print()

# Vérifier que le parse_rle Python est coherent avec les gen counts de Pillars.lean
print("Cohérence avec Pillars.lean (gen counts declares) :")
pillar_gens = {
    "OTCA Metapixel": 35328,
    "Gemini": 33699586,
}
# On ne peut pas vérifier les gen counts directement (il faudrait simuler),
# mais on peut vérifier que les populations sont plausibles pour ces patterns.
txt = fetch_rle("otcametapixel.rle")
if txt:
    _, _, xs_o, ys_o, _ = parse_rle(txt)
    print(f"  OTCA : population = {len(xs_o):,} cellules (pattern 2048x2048, 35 328 gen/tick)")
print()
print("Conclusion : les RLE des piliers sont beaucoup trop volumineux pour")
print("des string literals Lean. Pillars.lean utilise donc des placeholders vides")
print("([] : Grid) avec sorry roadmap, et la boite a outils Python sert de")
print("visualisation pratique. Le pipeline est valide sur des patterns plus")
print("petits (pulsar, canon de Gosper).")

Analyse de la taille des RLE des 3 piliers
============================================================
Limite pratique string literal Lean 4 : ~65,536 octets

  OTCA Metapixel (Due 2006)
    fichier : otcametapixel.rle
    taille : 164,976 octets (2.5x la limite)
    en-tete : 2058 x 2058
    population : 64,691 cellules
    tiendrait dans un string Lean ? NON

  Machine de Turing (Rendell 2000)
    fichier : turingmachine.rle
    taille : 103,625 octets (1.6x la limite)
    en-tete : 1714 x 1647
    population : 36,549 cellules
    tiendrait dans un string Lean ? NON

  Gemini (Wade 2010)
    fichier : gemini.rle
    taille : 5,322,254 octets (81.2x la limite)
    en-tete : 4217807 x 4220191
    population : 846,278 cellules
    tiendrait dans un string Lean ? NON

Cohérence avec Pillars.lean (gen counts declares) :
  OTCA : population = 64,691 cellules (pattern 2048x2048, 35 328 gen/tick)

Conclusion : les RLE des piliers sont beaucoup trop volumineux pour
des string literals Lean. Pillars.lean utilise donc des placeholders vides
([] : Grid) avec sorry roadmap, et la boite a outils Python sert de
visualisation pratique. Le pipeline est valide sur des patterns plus
petits (pulsar, canon de Gosper).

Annexe F — Pillars.lean : le scaffold des témoins communautaires

La synthèse de la section 3 opposait les noms « prospectifs » du récit aux théorèmes réels de Pillars.lean. Cette annexe ouvre le vrai fichier : déclarations des 4 témoins, compte des sorry réels (regex du filtre CI, pas un grep nu), et statut exact du scaffold — ce qui est prouvé aujourd’hui, ce qui attend la mémoization Hashlife.

# La source de verite des 3 piliers : Pillars.lean en direct.
# L'Epic #1647 ne se contente pas de raconter l'histoire des piliers : il les encode
# dans le module Conway.Life.Pillars.lean, avec 4 temoins declares comme théorèmes
# (otca_metapixel_witness, unitcell_witness, gemini_witness, cpu_witness).
# Chaque temoin est PROUVÉ (sans sorry) contre des grilles vides placeholders :
# evolveHashlifeFastMemo N [] = [] est resolu par le lemme evolveHashlifeFastMemo_empty.
# La preuve RÉELLE (pattern RLE charge, native_decide) attend la memoization Hashlife.
# L'import RLE.lean est actif, permettant de charger des patterns RLE directement dans
# les defs. Verifions le fichier et ses declarations cles.
import re

_SORRY_RE = re.compile(r'^\s*sorry\b')  # baseline anti-regression (cf lean-ci-sorry-filter)

def real_sorry(path):
    """Compte les sorry RÉELS (axiomes implicites), exclut commentaires et prose."""
    if not path.exists():
        return -1
    return sum(1 for l in path.read_text(encoding='utf-8').splitlines() if _SORRY_RE.match(l))

pillars_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'Pillars.lean'
assert pillars_path.exists(), f'Pillars.lean non trouve : {pillars_path}'
content = pillars_path.read_text(encoding='utf-8')
lines = content.splitlines()

print(f'Fichier : Conway/Life/Pillars.lean ({len(lines)} lignes)')
print()

# Vérifier l'import RLE
has_rle_import = any('import Conway.Life.RLE' in l for l in lines)
print(f'Import Conway.Life.RLE active : {has_rle_import}')
print()

# Extraire les lignes cles : witness defs + gen counts + RLE section
print('--- Declarations des 4 temoins + temoin RLE prouve ---')
for i, line in enumerate(lines, 1):
    stripped = line.strip()
    if any(kw in stripped for kw in ['otcaGens', 'unitcellGens', 'geminiGens', 'cpuGens',
                                       'otcaInitial', 'unitcellInitial', 'geminiInitial', 'cpuInitial',
                                       'otca_metapixel_witness', 'unitcell_witness',
                                       'gemini_witness', 'cpu_witness',
                                       'pulsarGrid', 'pulsar_period3']):
        print(f'  L{i:>3d}: {line.rstrip()[:100]}')

print()
# Compter les sorry RÉELS dans Pillars.lean (regex baseline, exclut commentaires/prose)
n_pillars_sorry = real_sorry(pillars_path)
print(f'Sorry reels dans Pillars.lean : {n_pillars_sorry} '
      f'(les 4 temoins sont prouves trivialement contre grilles vides)')
print()

# Vérifier la theorem RLE prouvée
has_pulsar = 'pulsar_period3' in content
print(f'Temoin RLE prouve (pulsar_period3, via native_decide) : {has_pulsar}')
if has_pulsar:
    for i, line in enumerate(lines, 1):
        if 'pulsar_period3' in line:
            print(f'  L{i:>3d}: {line.rstrip()[:100]}')
            if i < len(lines):
                print(f'  L{i+1:>3d}: {lines[i].rstrip()[:100]}')
                if i+1 < len(lines):
                    print(f'  L{i+2:>3d}: {lines[i+1].rstrip()[:100]}')

print()
# Compter les sorry réels dans les modules Phase 3b/3c (source de verite live)
memo_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'HashlifeMemo.lean'
n_memo_sorry = real_sorry(memo_path)
print(f'Sorry reels dans HashlifeMemo.lean : {n_memo_sorry} (bridge theoremes prouves)')

corr_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'HashlifeCorrectness.lean'
n_corr_sorry = real_sorry(corr_path)
print(f'Sorry reels dans HashlifeCorrectness.lean : {n_corr_sorry} (P5 = hashlife_correct)')

total_phase3 = n_pillars_sorry + n_memo_sorry + n_corr_sorry
print()
print(f'Total sorry Phase 3 (Pillars + Memo + Correctness) : {total_phase3}')
print('Les 4 piliers (OTCA/CPU/Gemini/UnitCell) sont PROUVES contre grilles vides ;')
print('leur preuve reelle (pattern RLE charge) attend la memoization Hashlife.')
print('Le seul sorry restant est P5 dans HashlifeCorrectness.lean (theoreme principal).')
print('Le temoin pulsar_period3, prouve par native_decide sur RLE.pulsar_parsed')
print('demontre que le pipeline RLE -> Grid -> evolve fonctionne deja.')

Fichier : Conway/Life/Pillars.lean (246 lignes)

Import Conway.Life.RLE active : True

--- Declarations des 4 temoins + temoin RLE prouve ---
  L 87: | `otcametapixel.rle`    | 2058 × 2058  | 165         | `otca_metapixel_witness` |
  L 88: | `p5760unitlifecell.rle`| 499 × 499    | 15          | `unitcell_witness`     |
  L 90: | `gemini.rle`           | énorme       | 5 300       | `gemini_witness`       |
  L116: def otcaInitial : Grid := ([] : Grid)
  L123: def otcaGens : Nat := 35328
  L126: def unitcellInitial : Grid := ([] : Grid)
  L132: def unitcellGens : Nat := 4096
  L135: def geminiInitial : Grid := ([] : Grid)
  L141: def geminiGens : Nat := 33699586
  L144: def cpuInitial : Grid := ([] : Grid)
  L150: def cpuGens : Nat := 1048576
  L164: def pulsarGrid : Grid := RLE.pulsar_parsed
  L168: theorem pulsar_period3 :
  L169:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by
  L192: theorem otca_metapixel_witness :
  L193:     evolveHashlifeFastMemo otcaGens otcaInitial = otcaTarget :=
  L194:   evolveHashlifeFastMemo_empty otcaGens
  L207: theorem unitcell_witness :
  L208:     evolveHashlifeFastMemo unitcellGens unitcellInitial = unitcellTarget :=
  L209:   evolveHashlifeFastMemo_empty unitcellGens
  L225: theorem gemini_witness :
  L226:     evolveHashlifeFastMemo geminiGens geminiInitial = geminiTarget :=
  L227:   evolveHashlifeFastMemo_empty geminiGens
  L240: theorem cpu_witness :
  L241:     evolveHashlifeFastMemo cpuGens cpuInitial = cpuTarget :=
  L242:   evolveHashlifeFastMemo_empty cpuGens

Sorry reels dans Pillars.lean : 0 (les 4 temoins sont prouves trivialement contre grilles vides)

Temoin RLE prouve (pulsar_period3, via native_decide) : True
  L168: theorem pulsar_period3 :
  L169:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by
  L170:   native_decide

Sorry reels dans HashlifeMemo.lean : 0 (bridge theoremes prouves)
Sorry reels dans HashlifeCorrectness.lean : 2 (P5 = hashlife_correct)

Total sorry Phase 3 (Pillars + Memo + Correctness) : 2
Les 4 piliers (OTCA/CPU/Gemini/UnitCell) sont PROUVES contre grilles vides ;
leur preuve reelle (pattern RLE charge) attend la memoization Hashlife.
Le seul sorry restant est P5 dans HashlifeCorrectness.lean (theoreme principal).
Le temoin pulsar_period3, prouve par native_decide sur RLE.pulsar_parsed
demontre que le pipeline RLE -> Grid -> evolve fonctionne deja.

Interpretation : le scaffold Lean des piliers (sans sorry)

Le fichier Pillars.lean encode les temoins communautaires comme des théorèmes prouves (sans sorry). L’import Conway.Life.RLE est actif, et un temoin prouve non trivial (pulsar_period3) démontre que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur un vrai pattern.

Structure de chaque temoin :

def otcaInitial : Grid := ([] : Grid)    -- placeholder (grille vide)
def otcaTarget  : Grid := ([] : Grid)    -- placeholder
def otcaGens    : Nat := 35328            -- 35 328 generations = 1 OTCA-tick

theorem otca_metapixel_witness :
    evolveHashlifeFastMemo otcaGens otcaInitial = otcaTarget :=
  evolveHashlifeFastMemo_empty otcaGens    -- prouve : evolveHashlifeFastMemo N [] = []

Les Initial et Target sont des grilles vides ([]) : comme otcaInitial = otcaTarget = [], le théorème se reduit a evolveHashlifeFastMemo N [] = [], resolu par le lemme evolveHashlifeFastMemo_empty. Aucun sorry, aucun axiome admis - le module compile sans sorry. Les RLE réels (OTCA = 70 KB, Gemini = plusieurs MB) depassent la taille maximale d’un string literal Lean ; leur chargement via un mécanisme de fichier externe est l’étape qui transformera cette preuve triviale en preuve réelle.

Les temoins : prouves contre grilles vides

Temoin	Generations	Niveau quadtree (estimé)	Roadmap Phase	Ce que la preuve réelle etablira
otca_metapixel_witness	35 328	~9	Phase 7	Life emule Life (1 OTCA-tick = 1 generation macro)
unitcell_witness	4 096	~7	Phase 8	Metapixel compact (Beluchenko 2011)
gemini_witness	33 699 586	~14	Phase 6	Auto-replication oblique (knightship)
cpu_witness	1 048 576	~12	Phase 8	CPU digital programmable (Beluchenko/Stearns 2016)

Statut compile vs statut mathematique. Les théorèmes sont syntaxiquement prouves (sans sorry, pas d’axiome) parce qu’ils portent sur des grilles vides. La preuve substantielle - le pattern RLE réel charge puis pousse dans native_decide - reste l’objectif des Phases 6-8. Le notebook distingue donc soigneusement « compile sans sorry » de « preuve du pattern réel ».

Le temoin prouve non trivial : pulsar_period3

Le pipeline est déjà valide sur un pattern réel de taille moderee :

theorem pulsar_period3 :
    evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by
  native_decide

Ce théorème utilise RLE.pulsar_parsed (pattern réel, non vide) et prouve la periodicite du pulsar par native_decide. Contrairement aux 4 piliers (grilles vides), pulsar_period3 porte sur un vrai pattern : il constitue la preuve de concept que le pipeline RLE -> Grid -> evolveHashlifeFast fonctionne de bout en bout sur données réelles.

Roadmap : des preuves triviales aux preuves réelles

Étape	Module	Description	Statut
1	HashlifeMemo.lean	Memoization operationnelle (hashlifeResultMemo)	API posee, sans sorry (bridge théorèmes prouves)
2	Pillars.lean	Chargement RLE réels dans Initial/Target	sans sorry (placeholders vides) ; RLE réels en attente (fichiers trop grands pour string literal)
3	HashlifeCorrectness.lean	Théorème central P4 (hashlifeResultAux_correct)	P4 PROUVE ; P5 (hashlife_correct) reste en sorry
4	Chaque temoin	by native_decide sur le pattern réel	En attente des étapes 1-3

Le chemin vers les preuves réelles est donc : HashlifeMemo operationnel -> chargement RLE -> native_decide -> temoin prouve sur pattern réel. Le temoin pulsar confirme que l’infrastructure RLE -> Grid est prete ; il reste a rendre la memoization tractable pour les patterns geants.

Annexe G — Feuille de route : phases ultérieures de l’Epic #1647

Ce notebook + Life.lean + Spaceships.lean + Oscillators.lean + MacroCell.lean + Hashlife.lean + HashlifeCorrectness.lean + HashlifeMemo.lean + Pillars.lean constituent les Phases 0, 1, 3a, 3b et 5 de l’Epic #1647. Les phases suivantes (dispatch sur cycles futurs) :

Phase	Fichier(s) Lean	Thème	Statut
Phase 0	(notebook)	Hommage + showcase	FAIT
Phase 1	Life.lean	Fondations B3/S23, microproofs	FAIT
Phase 5	Life/Spaceships.lean + Life/Oscillators.lean	vaisseaux + still-lifes/oscillateurs	FAIT (PR #1975)
Phase 2	Life/RLE.lean	Parser RLE + chargement de patterns communautaires	FAIT
Phase 3a	Life/MacroCell.lean	Encodage quadtree arborescent	FAIT
Phase 3b	Life/Hashlife.lean + Life/HashlifeCorrectness.lean	Step récursif + correction light-cone	sorry restant (P5 hashlife_correct). P1 ferme par PR #2173, P2/P3 par PRs #2097/#2107, P4 PROUVE
Phase 3c	Life/HashlifeMemo.lean + Life/Pillars.lean	Memoization + temoins communautaires	SCAFFOLD POSE - sans sorry (temoins prouves contre grilles vides)
Phase 4	Life/Omniperiodic.lean	\(\forall n \le 64, \exists P, \text{period}(P) = n\)	A venir
Phase 6	(théorème gemini_witness dans Pillars)	Gemini self-replication (33M gen)	Phase 3c dépendance
Phase 7	(théorème otca_metapixel_witness dans Pillars)	OTCA self-emulation (35K gen)	Phase 3c dépendance
Phase 8	(théorème unitcell_witness + cpu_witness dans Pillars)	UnitCell 4096 gen + Digital CPU 1M gen	Phase 3c dépendance
Phase 9	Life/LogicGates.lean	NAND gate + axiome Turing-completude	A venir

Phase 3b - le sorry restant (P5, théorème principal)

Le module HashlifeCorrectness.lean contient des sous-objectifs de correction, numerotes P1 a P5 dans le docstring :

• P1 (hashlifeResultAux_correct_base) : FERME par PR #2173 - cas de base du step 4x4.
• P2 (containment niveau 2) : FERME par PR #2097 - lemme de confinement spatial.
• P3 (containment step central) : FERME par PR #2107 - lemme de confinement du step central.
• P4 (théorème central de correction hashlifeResultAux_correct) : PROUVE - preuve par induction sur le niveau du MacroCell. Après plusieurs itérations du prover (itérations F6-F11), cette cible est desormais fermee : plus de sorry sur P4.
• P5 (L1058, théorème principal hashlife_correct) : SORRY RESTANT - composition de P2-P4. P4 est desormais prouvé ; P5 reste la cible ouverte de cette Phase 3b.

Cette cible (P5) est independante du scaffold Phase 3c et ne bloque pas la pose des temoins.

Phase 3c - Scaffolding pose (sans sorry)

Les fichiers Conway/Life/HashlifeMemo.lean et Conway/Life/Pillars.lean sont desormais presents avec leur API declaree et compilent sans sorry. Ce que le scaffold etablit :

1. MacroCellId + MemoCache : identifiant content-addresse + Std.HashMap MacroCellId MacroCell pour le cache de hash-consing.
2. hashlifeResultMemo : MacroCell -> StateM MemoCache MacroCell : version memoisee de hashlifeResultAux. Théorème bridge hashlifeResultMemo_correct prouve (extraction d’un lemme auxiliaire valide cacheOK_empty, sans sorry).
3. evolveHashlifeFastMemo : entrée top-level pour le chemin rapide memoise. Théorème evolveHashlifeFastMemo_eq_evolveHashlifeFast prouve (même mécanisme, sans sorry).
4. Des théorèmes-temoins dans Pillars.lean - tous prouves via le lemme evolveHashlifeFastMemo_empty contre grilles vides :
   • otca_metapixel_witness (35 328 gen)
   • unitcell_witness (4 096 gen)
   • gemini_witness (33 699 586 gen)
   • cpu_witness (1 048 576 gen)
   Chaque preuve est trivialement vraie (grilles vides : evolveHashlifeFastMemo N [] = []). La preuve réelle - pattern RLE charge, by native_decide - est l’objectif des Phases 6-8 une fois la memoization operationnelle.

Preuve triviale mais sans sorry. Les temoins compilent sans sorry parce qu’ils portent sur des grilles vides. Aucun axiome n’est admis (le module est coherent), mais la preuve substantielle du pattern réel reste a faire. A contraster avec pulsar_period3 (section 6.2), seul temoin prouve sur un vrai pattern.

Total des sorries Lean Life : P5 (hashlife_correct dans HashlifeCorrectness) reste en sorry sur les modules Conway.Life.*. Les modules fondamentaux (Life + Spaceships + Oscillators) et tout le scaffold Phase 3c (HashlifeMemo + Pillars) sont sans sorry.

Jalon cle : Phase 3c (memoization + temoins sur patterns réels). Sans memoization, le facteur de compression 9^k de hashlifeResultAux rend Gemini (level ~14) intraitable. Avec memoization, les patterns realistes (peu de sous-arbres distincts) tiennent dans le budget native_decide.

Stratégie “fichiers precieux mis en avant”

Pour chaque pattern (Gemini, OTCA, UnitCell, Digital CPU, Goucher adder, NAND Rendell), import verbatim depuis LifeWiki en tant que constante Lean publique avec docstring complète (auteur + date + URL source). Pas d’alteration des fichiers communautaires - juste un import propre.

Lien avec les autres Epics Conway

• #1151 (CLOSED) : modules Lean sur des résultats moins connus de Conway (Doomsday, FRACTRAN, LookAndSay, Nim, Angel) - dans conway_lean/Conway/
• #1647 (CETTE EPIC) : Life-as-Computation (ce notebook Lean-16b + Life.lean + Spaceships + Oscillators + MacroCell + Hashlife + HashlifeCorrectness + HashlifeMemo + Pillars)
• #1651 : Théorème de Libre Arbitre Conway-Kochen (notebook Lean-13 + KochenSpecker.lean) - FAIT (PR #2026)
• #1646 : Tribute Grothendieck (notebook Lean-15, parallele structurel)