“Conway n’aimait pas qu’on le reduise a ce qu’il avait de plus connu comme le Game of Life, alors qu’il a des résultats beaucoup plus profonds.”
Objectifs d’apprentissage
Situer l’ampleur de l’oeuvre de Conway au-dela du Game of Life (surreels, Moonshine, noeuds, spheres, pavages, théorie des nombres)
Exécuter et interpreter les preuves Lean 4 réelles formalisees dans conway_lean/
Relier chaque résultat Lean au théorème mathematique correspondant (Doomsday, Look-and-Say, Nim, Ange, Life)
Decouvrir le tour CGT importe depuis vihdzp/combinatorial-games (nombres surreels, nimbers)
Prerequis
Python 3.10+ (numpy, matplotlib non requis ici)
WSL + Lake (pour la compilation Lean en section 3)
Aucun prerequis Lean (le notebook lit les fichiers .lean du depot)
Duree estimée
~120 minutes (lecture du panorama + compilation des 5 noix + CGT Tour)
John Horton Conway (1937-2020) est l’un des mathematiciens les plus inventifs du XXe siecle. Le grand public ne retient souvent que son Jeu de la Vie (Game of Life), un automate cellulaire de 1970. Mais Conway lui-même considerait cette invention comme mineure au regard de son oeuvre.
En une carriere, il a : refonde la théorie des jeux combinatoires et decouvert avec elle une nouvelle classe de nombres (les nombres surreels) ; mis au jour trois groupes sporadiques en dissequant le reseau de Leech ; co-formule la conjecture du Monstrous Moonshine reliant le plus grand groupe sporadique a la fonction modulaire \(j\) ; donne son nom au nœud de Conway (dont la non-trivialite “lisse” ne sera tranchée qu’en 2020) ; reformule le polynome d’Alexander en théorie des noeuds ; et contribue de maniere decisive a l’empilement de spheres en dimension 24. Le Game of Life n’est qu’une facette de cette oeuvre, pas son centre de gravite.
Ce notebook mene par la profondeur : on parcourt d’abord le panorama de ces grands résultats, puis on exécute les preuves Lean 4 réelles déjà formalisees dans conway_lean/ — sans paraphrase, en lisant et en compilant les fichiers .lean du depot (single source of truth).
Place dans la serie
Notebook
Thème
Statut
Lean-16a (ce notebook)
Conway, l’homme et l’oeuvre — panorama + premières noix crackees
Premières noix crackees : exécution des .lean réels (Doomsday, Look-and-Say, Nim, Ange, Life, CGT)
Trois exercices
1. Biographie et style singulier
Ne a Liverpool le 26 decembre 1937, John Horton Conway etudie a Cambridge (Gonville & Caius College), ou il soutient en 1964 une these de théorie des nombres sous la direction d’Harold Davenport. Il y enseigne jusqu’en 1986, gagnant une reputation de conferencier hors norme, avant de rejoindre Princeton comme titulaire de la chaire John von Neumann de mathematiques. Il meurt le 11 avril 2020 des suites du COVID-19. Elu Fellow of the Royal Society des 1981, il recoit notamment le prix Berwick (1971), le prix Polya de la LMS (1987) et le prix Nemmers (1998).
Son style mathematique est unique : le jeu comme méthode. La ou d’autres voient un divertissement, Conway voit une structure profonde a formaliser. Le Jeu de la Vie n’est pas une recreation : c’est une machine de Turing universelle deguisee. Les jeux a deux joueurs (Nim, Hackenbush, Domineering) ne sont pas des passe-temps : ils engendrent une arithmetique complète — les nombres surreels.
Cette espieglerie au service de la profondeur caractérise toute son oeuvre. Conway aimait inventer des notations frappantes (la fleche chainee de Conway pour les très grands nombres, la notation des groupes), des noms imagees (le “Monstre”, les “lutins” / sprouts, les “noix” qu’il “craquait”), et des algorithmes que l’on peut exécuter de tete — il avait d’ailleurs programme son ordinateur pour le soumettre, a chaque connexion, a un test chronometre de l’algorithme Doomsday. Mais derriere le showman se cache un theoricien de premier plan : il detestait justement que le Game of Life eclipse, aupres du public, des résultats qu’il jugeait bien plus importants.
Trois livres jalonnent son oeuvre accessible :
On Numbers and Games (1976) — les nombres surreels et la théorie des jeux combinatoires.
Winning Ways for Your Mathematical Plays (1982, avec Berlekamp et Guy) — la bible des jeux combinatoires.
Sphere Packings, Lattices and Groups (1988, avec Sloane) — “SPLAG”, reseaux et groupes.
Sa vie et sa personnalite sont racontees dans la biographie de Siobhan Roberts, Genius at Play (2015).
2. Panorama des grands résultats
Conway a laisse une empreinte dans des domaines extraordinairement varies : théorie des jeux, théorie des nombres, théorie des groupes finis, geometrie des reseaux, topologie de basse dimension, théorie des automates, logique. En voici un tour d’horizon — c’est cette largeur, et la profondeur de chaque contribution, que l’Epic met en avant, et non le seul Game of Life. Plusieurs de ces résultats sont formalises en Lean dans la section 3 ; les autres situent l’ampleur de l’oeuvre.
2.1 Les nombres surreels
Dans On Numbers and Games (ONAG), Conway construit a partir des jeux combinatoires une classe de nombres, les nombres surreels (notes No), qui contient simultanement les réels, les ordinaux transfinis et une hiérarchie d’infinitesimaux. Chaque nombre nait d’une paire \(\{L \mid R\}\) d’ensembles de surreels déjà construits, soumise a la seule contrainte qu’aucun élément de \(L\) ne soit \(\geq\) a un élément de \(R\). Deux règles — une comparaison et une addition — suffisent alors a tout engendrer.
La construction procede par “jours de naissance” : le jour 0 ne contient que \(0=\{\mid\}\) ; le jour 1 ajoute \(1=\{0\mid\}\) et \(-1=\{\mid 0\}\) ; les jours finis donnent tous les rationnels dyadiques ; le jour \(\omega\) livre d’un coup tous les réels et l’ordinal \(\omega=\{0,1,2,\dots\mid\}\), suivi des exotiques \(\tfrac1\omega=\{0\mid 1,\tfrac12,\tfrac14,\dots\}\), \(\omega-1\), \(\sqrt\omega\), etc. On obtient ainsi le plus grand corps totalement ordonné possible (un corps réel clos, “universel” : tout corps ordonné s’y plonge), si vaste qu’il forme une classe propre et non un ensemble.
Le coup de genie d’ONAG est que cette construction est la même que celle des jeux : un surreel est un jeu particulier (celui ou tout \(L\) reste $< $ tout \(R\)). Des jeux comme \(\ast=\{0\mid 0\}\) (l’etoile de Nim) ne sont pas des nombres, mais habitent le même univers — ce qui fait des nombres surreels le socle de toute la théorie des jeux combinatoires (valeurs, temperatures, thermographie de Winning Ways). Donald Knuth a popularise l’idee dans son roman mathematique Surreal Numbers (1974), ou il forge d’ailleurs le terme “surreal”.
2.2 Groupes de Conway, le Monstre et le Monstrous Moonshine
Les groupes de Conway. En 1968, Conway etudie les symetries du reseau de Leech\(\Lambda_{24}\) (cf. 2.3) et calcule son groupe d’automorphismes \(\mathrm{Co}_0 = \mathrm{Aut}(\Lambda_{24})\), d’ordre
Ce groupe n’est pas simple (son centre est \(\{\pm 1\}\)), mais le quotient \(\mathrm{Co}_1=\mathrm{Co}_0/\{\pm 1\}\) l’est — tout comme les stabilisateurs \(\mathrm{Co}_2\) et \(\mathrm{Co}_3\) de certains vecteurs du reseau. Ce sont trois des 26 groupes sporadiques simples. Au passage, Conway redecouvre et eclaire les groupes de Mathieu \(M_{12}, M_{24}\) via le code de Golay binaire \([24,12,8]\) et le Miracle Octad Generator.
La constellation du Monstre. Ces groupes s’inscrivent dans la classification des groupes finis simples (achevee vers 1983-2004). Le plus grand des sporadiques est le Monstre\(\mathbb{M}\), d’ordre \(\approx 8\times10^{53}\). Vingt des 26 sporadiques — dont les trois groupes de Conway — sont des sous-quotients du Monstre : Conway les surnomme la “Happy Family” ; les six autres sont les “parias”. Le catalogue de reference de tous ces groupes est l’ATLAS of Finite Groups (Conway, Curtis, Norton, Parker, Wilson, 1985).
Le Monstrous Moonshine. En 1978, John McKay remarque une coincidence stupefiante :
\[196884 = 196883 + 1,\]
ou \(196884\) est le premier coefficient de Fourier non trivial de la fonction modulaire\(j\) (\(j(\tau)=q^{-1}+744+196884\,q+\dots\), avec \(q=e^{2i\pi\tau}\)) et \(196883\) la dimension de la plus petite representation irreductible non triviale du Monstre. Conway et Simon Norton transforment l’anecdote en programme : leur conjecture du Monstrous Moonshine (1979) associe a chaque élément du Monstre une fonction modulaire de genre zero (un Hauptmodul). Frenkel, Lepowsky et Meurman construisent ensuite l’algebre vertex\(V^{\natural}\) (le “module moonshine”), dont les dimensions graduees redonnent exactement les coefficients de \(j\). Richard Borcherds démontre la conjecture en 1992 a l’aide d’algebres de Kac-Moody generalisees — travail couronne par la medaille Fields 1998. Ce pont inattendu entre théorie des groupes finis et formes modulaires reste l’un des grands mysteres feconds des mathematiques contemporaines.
« There are 26 dimensions in bosonic string theory. » – R. Borcherds [50:24] – la coïncidence qui relie le Monstre aux cordes bosoniques : 26 dimensions pour la théorie, dont 24 transverses, exactement la graduation où vivent les séries d’Eisenstein et le moonshine (cf. ../Langlands/02-monstrous-moonshine-invariant-j.ipynb).
2.3 Reseau de Leech et empilement de spheres
Le reseau de Leech\(\Lambda_{24}\) est un reseau exceptionnel de dimension 24, pair, unimodulaire et sans racine (aucun vecteur de norme 2, la norme minimale valant 4). Conway en a donné une construction limpide a partir du code de Golay binaire \([24,12,8]\), et c’est en calculant ses symetries qu’il met au jour les groupes de la section 2.2.
\(\Lambda_{24}\) réalise l’empilement de spheres le plus dense connu en dimension 24, avec un nombre de contact (kissing number) de 196 560 : chaque sphere en touche exactement 196 560 autres. L’optimalite de ce kissing number en dimension 24 (et en dimension 8 pour le reseau \(E_8\), ou il vaut 240) est etablie des 1979 par Odlyzko-Sloane et, independamment, Levenshtein.
L’optimalite de l’empilement lui-même — longtemps conjecturée, jamais prouvée — n’est tranchée qu’en 2016 par Maryna Viazovska : seule pour la dimension 8 (\(E_8\)), puis avec Cohn, Kumar, Miller et Radchenko pour la dimension 24 (\(\Lambda_{24}\)). La méthode, d’une elegance saisissante, construit des “fonctions magiques” d’interpolation via des formes modulaires, qui forcent l’inégalité de densite a saturer exactement sur ces reseaux. Ce résultat, prolongement direct de l’heritage de Conway et de SPLAG, vaut a Viazovska la medaille Fields 2022.
« I’ve heard you talk about deep holes in the Leech lattice. What are deep holes and how many are there? » – question posée à R. Borcherds, The most magical subject in math (2026, [51:24]) ; puis : « in Lorentzian space, the length of a vector can be imaginary if the vector is time-like… we’ve been talking about lattices up to 26 dimensions, but past that, things seem to kind of blow up » [1:23:15] – Conway et Borcherds ont ouvert ces questions ensemble : les trous profonds du Leech sont la porte d’entrée du moonshine lorentzien.
2.4 Théorie des noeuds : le polynome et le noeud de Conway
Le polynome de Conway. Conway reformule le polynome d’Alexander d’un noeud sous une forme calculable par une relation d’echeveau (skein relation) locale, donnant le polynome d’Alexander-Conway\(\nabla(z)\) :
\[\nabla(L_+) - \nabla(L_-) = z\,\nabla(L_0),\]
ou \(L_+, L_-, L_0\) sont trois diagrammes identiques sauf au voisinage d’un croisement, et avec la normalisation \(\nabla(\text{noeud trivial})=1\). Cette approche combinatoire et locale a ouvert la voie aux invariants modernes (polynome de Jones, HOMFLY).
Le noeud de Conway. Conway donne aussi son nom à un nœud célèbre à 11 croisements (note \(11n34\)), obtenu par mutation a partir du noeud de Kinoshita-Terasaka. Sa particularite : il possede un polynome d’Alexander trivial (egal a celui du noeud trivial), ce qui le rend, par un théorème de Freedman, topologiquement slice — il borde un disque topologique plonge dans la boule de dimension 4. Restait la question, ouverte pres de cinquante ans : est-il lissement (smoothly) slice, c’est-a-dire borde-t-il un disque lisse ?
En 2020 (Annals of Mathematics), Lisa Piccirillo repond non. Son idee : deux noeuds qui partagent la même “trace” de dimension 4 sont simultanement slice ou non ; elle construit un noeud de même trace que le noeud de Conway, puis lui applique l’invariant \(s\) de Rasmussen (issu de l’homologie de Khovanov), qui obstrue la sliceness lisse. Le nœud de Conway était le dernier nœud à12 croisements ou moins dont le caractère slice restait inconnu. Cerise sur le gateau : son mutant de Kinoshita-Terasaka, lui, est slice — preuve eclatante que la mutation ne preserve pas la sliceness lisse.
2.4b Pavages : le critere de Conway et la notation orbifold
Le critere de Conway (Conway, 1992) est un critere suffisant pour qu’un polygone pave le plan par copies de lui-même (isometries directes uniquement — translations et rotations). C’est l’un des rares critères purement locaux : on n’a pas besoin d’examiner le pavage global, seulement la geometrie du bord du polygone.
Le critere dit qu’un polygone pave le plan si son bord peut etre decompose en six segments consécutifs \(A, B, C, D, E, F\) tels que :
Le bord \(A\) est une translation du bord \(D\) (ils sont paralleles, de même longueur et orientes dans le même sens).
Les bords \(B\) et \(C\) sont symetriques par rapport au milieu du segment reliant le point final de \(A\) au point initial de \(D\) (rotation a 180 degrés de \(B\) autour de ce milieu donné \(C\)).
De même, \(E\) et \(F\) sont symetriques par rapport au milieu du segment reliant le point final de \(D\) au point initial de \(A\).
Les conditions 2 et 3 signifient simplement que les paires \((B,C)\) et \((E,F)\) sont liees par des rotations de 180 degrés — legerement plus général que la reflexion. Si l’une des paires est vide (longueur nulle), le critere se simplifie et couvre les cas classiques (hexagones, parallelogrammes).
Le critere est suffisant mais pas necessaire : certains paveurs ne le satisfont pas. Cependant, il capture une proportion importante des paveurs connus et offre une vérification algorithmique simple. Il illustre une fois de plus le style de Conway : un critere verifiable localement, reposant sur une symetrie élémentaire, qui engendre une structure globale.
La notation orbifold. Conway invente aussi une notation pour les groupes de symetrie des pavages du plan, d’une economie remarquable. Au lieu de nommer les groupes par les notations cristallographiques internationales (p4m, p6m, p2gg…), la notation orbifold encode directement la topologie du quotient du plan par le groupe de symetrie :
\(*\) introduit un point de symetrie miroir.
\(n\) (entier) encode un point de rotation d’ordre \(n\).
\(\times\) encode une symetrie glissante (glide reflection).
\(\circ\) encode une direction de translation independante.
Par exemple : - \(*632\) : le groupe du pavage triangulaire (mirroirs + rotations d’ordre 6, 3 et 2). - \(632\) : même groupe sans mirroirs (rotations seules). - \(*2222\) : le groupe du pave carré avec mirroirs. - \(2*22\) : une variante du précédent. - \(\times\times\) : le groupe des glide reflections pures.
La beaute de cette notation est qu’elle est bijective : a chaque symbole correspond exactement un groupe de pavage du plan, et reciproquement. Conway l’etend aux pavages de la sphere et du plan hyperbolique, unifiant les trois geometries sous un même langage. Les 17 groupes cristallographiques du plan euclidien correspondent a exactement 17 symboles orbifolds distincts — une enumeration complète que la notation rend naturelle plutôt qu’arbitraire.
Cette contribution s’inscrit dans la même lignee que les groupes de Conway (section 2.2) et le reseau de Leech (section 2.3) : la capacite de Conway a voir et encoder les symetries d’une maniere qui les rend a la fois calculables et memorables.
2.5 Algorithme Doomsday
L’algorithme Doomsday (1973) permet de calculer de tete le jour de la semaine de n’importe quelle date. L’idee : dans chaque annee, certaines dates “ancres” tombent toutes le même jour, le Doomsday de l’annee — par exemple 4/4, 6/6, 8/8, 10/10, 12/12, le dernier jour de fevrier, ou encore 9/5 et 5/9 (mnemonique : “I work from 9 to 5 at the 7-Eleven”). On determine le Doomsday du siecle (mercredi pour les annees 1900, mardi pour les annees 2000), on le corrige de l’annee dans le siecle, puis on se deplace modulo 7 jusqu’a la date cherchee. C’est l’archetype de la mathematique “jouable” de Conway, qui s’entraînait à répondre en quelques secondes. Le 11 avril 2020, jour de sa mort, était justement un samedi — clin d’oeil que le fichier Lean encode comme théorème dayOfWeek_conway_death. On en formalise une version en Lean (section 3).
2.6 Constante de Look-and-Say
La suite “look-and-say” se lit a voix haute : \(1, 11, 21, 1211, 111221, 312211, \dots\) (on decrit le terme précédent : “un 1” -> 11, “deux 1” -> 21, etc.). Conway démontre le théorème cosmologique : toute chaîne de depart se decompose, au bout d’un nombre fini d’étapes, en juxtaposition de 92 “éléments” atomiques — qu’il baptise du nom des éléments chimiques, de l’hydrogene a l’uranium, plus deux éléments “transuraniens” pour les chiffres autres que 1, 2, 3 — une “desintegration audioactive”. Surtout, le rapport des longueurs de termes consécutifs converge vers la constante de Conway\(\lambda \approx 1{,}303577269\dots\), unique racine réelle positive d’un polynome de degré 71, et ce quelle que soit la graine de depart (a l’exception de la suite vide et de “22”). On en formalise des cas en Lean (section 3).
2.7 FRACTRAN
FRACTRAN (Conway, 1987) est un langage de programmation esoterique d’une economie radicale : un programme est une simple liste de fractions. Partant d’un entier \(n\), on le multiplie par la première fraction de la liste qui donne encore un entier, et l’on recommence ; le calcul s’arrete des qu’aucune fraction ne convient. Les entiers manipules encodent l’état d’une machine a registres via les exposants de leur factorisation première, ce qui rend FRACTRAN Turing-complet malgre sa syntaxe minuscule. Le programme PRIMEGAME de Conway (14 fractions) engendre, dans les puissances successives de 2 qu’il produit, la suite de tous les nombres premiers — un compilateur de l’arithmetique qui tient sur une seule ligne.
2.7b Le 15-théorème et les formes quadratiques
Le 15-théorème (Conway-Schneeberger, 1993, publie 2000) est l’un des résultats les plus profonds de Conway en théorie des nombres. Il caractérise les formes quadratiques positives universelles :
Si une forme quadratique définie positive a coefficients entiers represente les nombres1, 2, 3, 5, 6, 7, 10, 14 et 15, alors elle represente tous les entiers positifs.
L’enonce est d’une simplicite trompeuse. Une forme quadratique \(Q(x_1, \dots, x_n) = \sum a_{ij} x_i x_j\) (representee par la matrice symetrique des \(a_{ij}\)) represente l’entier \(k\) s’il existe des entiers \(x_1, \dots, x_n\) tels que \(Q(x_1, \dots, x_n) = k\). Dire qu’elle est universelle signifie qu’elle represente tout entier positif.
L’histoire commence avec Legendre (1798) : la forme \(x^2 + y^2 + z^2 + w^2\) represente tout entier positif (la “somme de quatre carrés”). Ramanujan (1917) enumere les 54 formes diagonales \(x^2 + ay^2 + bz^2 + cw^2\) universelles. Conway et Schneeberger montrent que pour les formes générales (matrice symetrique quelconque, pas seulement diagonale), il suffit de vérifier les neuf “temoins” ci-dessus.
Pourquoi c’est profond. La demonstration originale de Conway-Schneeberger est longue et difficile. En 2005, Manjul Bhargava — qui recoit la medaille Fields 2014 pour cette ligne de recherche — simplifie radicalement la preuve et généralise le résultat au 290-théorème : si une forme quadratique entière represente les 29 temoins de l’ensemble
alors elle represente tout entier positif par une forme entière (pas seulement a coefficients dans \(\mathbb{Z}\)). Le saut de 15 a 290 temoins s’explique par le passage des formes a coefficients dans \(\mathbb{Z}\) aux “formes entières” au sens large (le gradient prend des valeurs entières).
La connexion avec l’oeuvre de Conway est multiple : les formes quadratiques interviennent dans le reseau de Leech (section 2.3) et les groupes de Conway (section 2.2), et le 15-théorème s’inscrit dans la tradition de la théorie des nombres combinatoire qui traverse toute son oeuvre.
2.8 Problème de l’Ange
Le problème de l’Ange (Conway, 1982) oppose un Ange de puissance \(k\) (qui saute jusqu’a \(k\) cases en distance de Chebyshev) a un Diable qui detruit une case du plan a chaque tour. L’Ange peut-il echapper indefiniment, ou le Diable finit-il toujours par l’enfermer ? Conway met une prime de 1000 $ sur la question, longtemps tenue pour difficile (un Ange de puissance 1, le simple “roi”, perd). Elle est résolue indépendamment en 2006 par quatre auteurs — Brian Bowditch, Oddvar Kloster, Andras Mathe et Peter Gacs : un Ange de puissance \(\geq 2\)gagne toujours. On formalise la combinatoire du moveset en Lean (section 3) : un Ange de puissance \(k\) dispose de \((2k+1)^2-1\) cases d’arrivee.
2.9 Sprouts et le théorème du libre arbitre
Sprouts : un jeu topologique de papier-crayon invente par Conway et Michael Paterson en 1967, ou l’on relie des points par des courbes sans croisement, chaque point ne pouvant porter plus de trois aretes. Derriere des règles enfantines se cache une théorie combinatoire etonnamment riche : le nombre de positions explose vite, et la determination du gagnant pour un grand nombre de points initiaux reste un sujet de calcul informatique.
Théorème du libre arbitre (Conway-Kochen, 2006) : si les experimentateurs jouissent d’un “libre arbitre” (leurs choix de mesure ne sont pas une fonction du passe), alors certaines particules élémentaires en jouissent aussi — la réponse d’une particule ne saurait être prédéterminée. Ce résultat s’appuie sur le théorème de Kochen-Specker (contextualite quantique), objet du notebook Lean-13, et debouche sur le théorème du libre arbitre proprement dit, formalise dans Lean-16f.
3. Premières noix crackees : les preuves Lean réelles
On passe maintenant a la formalisation. Le projet conway_lean/ du depot contient des preuves Lean 4 (sur Mathlib) de plusieurs résultats de Conway, toutes a 0 sorry (aucun trou de preuve).
Plutot que de paraphraser, ce notebook lit et compile les fichiers .lean réels :
Thème
Fichier
Contenu
Doomsday
Conway/DoomsdayLemmas.lean
5 théorèmes (annees bissextiles, jour de la mort de Conway)
Look-and-Say
Conway/LookAndSayLemmas.lean
3 théorèmes (chiffres <-> entier, terme 4)
Nim / nim-sum
Conway/Nim.lean
defs + 4 théorèmes + #eval
Problème de l’Ange
Conway/Angel.lean
defs + 4 théorèmes (cardinal du moveset) + #eval
Game of Life (Phase 1)
Conway/Life.lean
7 micro-preuves (block, blinker, glider…)
MathlibMap
Conway/MathlibMap.lean
10 #check Conway-adjacents dans Mathlib
Le depot heberge aussi un second projet Lake indépendant, conway_cgt_lean/ (toolchain v4.31.0-rc2), qui importe vihdzp/combinatorial-games et presente les résultats centraux de Conway en théorie des jeux :
Thème
Fichier
Contenu
CGT Tour
CGTTour.lean
13 #check (jeux, surreels, nimbers) depuis vihdzp/combinatorial-games
Le pattern d’exécution repose sur WSL + Lake (cf. Lean-16b et Lean-12). La detection de chemin rend le notebook portable : il tourne sur n’importe quelle machine (lettre de lecteur c:, d:…) sans hardcode /mnt/c/.
# Setup : detection de chemin portable + helper WSL/Lake (single source of truth)import sysimport refrom 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, win_to_wsl, run_lake, count_sorry,)# Backward-compatible aliases for cells later in this notebookWIN_LEAN_PROJECT = find_lean_project('conway_lean')LEAN_PROJECT = get_lean_project_path('conway_lean')def wsl(cmd, timeout=60):"""Exécute une commande bash dans WSL Ubuntu (backward-compatible wrapper)."""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.stderrexcept subprocess.TimeoutExpired:return-1, '', f'TIMEOUT apres {timeout}s'exceptFileNotFoundError:return-2, '', 'WSL introuvable (notebook concu pour Windows + WSL Ubuntu)'print(f"Projet Lean (Windows) : {WIN_LEAN_PROJECT}")print(f"Projet Lean (WSL) : {LEAN_PROJECT}")print(f"Toolchain : {(WIN_LEAN_PROJECT /'lean-toolchain').read_text(encoding='utf-8').strip()}")assert (WIN_LEAN_PROJECT /'lakefile.lean').exists(), 'conway_lean/lakefile.lean introuvable'
Projet Lean (Windows) : <repo>MyIA.AI.Notebooks\SymbolicAI\Lean\conway_lean
Projet Lean (WSL) : <repo>MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean
Toolchain : leanprover/lean4:v4.32.1
# Helpers de lecture single-source-of-truth des .lean (lecture directe du depot)DECL_RE = re.compile(r"^\s*(theorem|lemma|def|abbrev|instance)\s+([\w'À-ſ]+)")def count_real_sorry(text: str) ->int:"""Compte les vrais `sorry` tactiques en excluant commentaires de ligne et blocs /- -/.""" n, in_block =0, Falsefor line in text.splitlines(): s = line.strip()if in_block:if'-/'in s: in_block =Falsecontinueif s.startswith('/-'):if'-/'notin s: in_block =Truecontinue code_part = s.split('--', 1)[0]if re.search(r'\bsorry\b', code_part): n +=1return ndef show_lean(relpath: str, max_lines: int=0):"""Affiche les declarations (theorem/def/...) d'un fichier .lean reel + comptage sorry.""" f = WIN_LEAN_PROJECT / relpath text = f.read_text(encoding='utf-8') decls = [(i +1, m.group(1), m.group(2))for i, l inenumerate(text.splitlines())for m in [DECL_RE.match(l)] if m] sorry = count_real_sorry(text)print(f"=== {relpath} ({len(text.splitlines())} lignes, sorry reels = {sorry}) ===")for ln, kind, name in decls:print(f" L{ln:>4}{kind:<8}{name}")if max_lines:print("-"*60)for l in text.splitlines()[:max_lines]:print(l)return sorry
3.1 Doomsday : Conway/DoomsdayLemmas.lean
L’algorithme Doomsday formalise. On vérifie notamment que Conway est mort un samedi (11 avril 2020), clin d’oeil que le fichier encode comme théorème dayOfWeek_conway_death.
show_lean('Conway/DoomsdayLemmas.lean')
=== Conway/DoomsdayLemmas.lean (52 lignes, sorry reels = 0) ===
L 31 theorem isLeapYear_2000
L 35 theorem isLeapYear_1900
L 39 theorem isLeapYear_2024
L 44 theorem dayOfWeek_conway_death
L 49 theorem dayOfWeek_add_seven
0
3.2 Look-and-Say : Conway/LookAndSayLemmas.lean
La conversion chiffres <-> entier et le calcul du 4e terme de la suite, prouvés par native_decide, plus une preuve par induction structurelle (digitsToNat_natToDigits).
show_lean('Conway/LookAndSayLemmas.lean')
=== Conway/LookAndSayLemmas.lean (62 lignes, sorry reels = 0) ===
L 32 theorem digitsToNat_example
L 36 theorem lookAndSay_4
L 41 theorem digitsToNat_natToDigits
0
3.3 Nim et nim-sum : Conway/Nim.lean
Le nim-sum (XOR des tas) est la cle de la théorie de Sprague-Grundy : une position de Nim est perdante pour le joueur au trait si et seulement si son nim-sum est nul. Le fichier contient les définitions, 4 théorèmes, et des #eval executables.
show_lean('Conway/Nim.lean')
=== Conway/Nim.lean (156 lignes, sorry reels = 0) ===
L 41 def nimSum
L 45 def isWinningNim
L 54 theorem nimSum_nil
L 57 theorem isWinningNim_345
L 61 theorem nimSum_single
L 65 theorem nimSum_self
L 86 theorem isWinningNim_357
L 97 theorem nimStrategy_357
L 102 theorem xor_zero
L 106 theorem xor_comm
L 110 theorem xor_assoc
L 114 theorem nimSum3_assoc
L 120 theorem winning_move_357
L 128 theorem losing_position_123
L 133 theorem all_moves_from_123_winning
L 144 theorem xor_reduce_3_1
L 148 theorem winning_move_verified_357
0
3.4 Problème de l’Ange : Conway/Angel.lean
On formalise la combinatoire du moveset de l’Ange : un Ange de puissance \(k\) dispose de \((2k+1)^2 - 1\) cases d’arrivee. Pour \(k=1\) (le “roi”), cela fait 8 cases ; pour \(k=2\), 24 cases. Le théorème général angelMoves_card etablit la formule pour tout \(k\).
show_lean('Conway/Angel.lean')
=== Conway/Angel.lean (77 lignes, sorry reels = 0) ===
L 41 def chebyshev
L 46 def angelMoves
L 55 theorem chebyshev_self
L 59 theorem kingMoves_card
L 63 theorem angelMoves2_card
L 69 theorem angelMoves_card
0
3.5 Game of Life - Phase 1 : Conway/Life.lean
Pour completude, les micro-preuves fondatrices du Jeu de la Vie : stabilite du block et de la ruche (still lifes), période 2 du blinker / toad / beacon (oscillateurs), et deplacement du glider (spaceship). L’approfondissement (Hashlife, RLE, computation universelle) est l’objet du notebook Lean-16b.
show_lean('Conway/Life.lean')
=== Conway/Life.lean (253 lignes, sorry reels = 0) ===
L 57 def lexLt
L 67 abbrev Grid
L 77 def mooreNeighbors
L 91 def isAlive
L 95 def liveNeighborCount
L 99 def aliveNext
L 107 def candidates
L 115 def lexLe
L 138 def sortDedup
L 146 theorem mem_sortDedup
L 152 def step
L 156 def evolve
L 174 def isStillLife
L 177 def isOscillator
L 180 def shift
L 185 def isSpaceship
L 200 def block
L 203 def beehive
L 206 def blinker_h
L 209 def blinker_v
L 212 def toad
L 215 def beacon
L 220 def glider
L 232 theorem block_still_life
L 235 theorem beehive_still_life
L 238 theorem blinker_period_two
L 241 theorem blinker_step
L 244 theorem toad_period_two
L 247 theorem beacon_period_two
L 250 theorem glider_spaceship
0
3.6 On compile tout : lake build Conway
La preuve ultime que ces résultats tiennent : le module Conway compile sans erreur ni sorry. On lance lake build Conway via WSL (timeout genereux ; a froid le build Mathlib peut etre long, auquel cas la vérification CI/PR fait foi). Toolchain : leanprover/lean4:v4.33.0.
# Build complet du module Conway (single source of truth : la compilation réelle)print("Lancement de `lake build Conway` via WSL (timeout 1500s)...")print("-"*60)rc, out, err = wsl(f'source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && lake build Conway 2>&1 | tail -20', timeout=1500,)print(out)if err and err.strip() andnot err.strip().startswith('TIMEOUT'):print('STDERR:', err[-300:])print()print(f"Exit code : {rc}")if rc ==0:print("SUCCESS : le module Conway compile (preuves valides, 0 sorry).")elif rc ==-1:print("TIMEOUT : build a froid trop long ici ; la verification CI/PR est autoritative.")else:print("Voir le log ci-dessus.")
Lancement de `lake build Conway` via WSL (timeout 1500s)...
------------------------------------------------------------
simp only [← hn̵e̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵sw_lvl, ← hse_lvl] at hb
Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Conway/Life/JumpCapture.lean:511:28: This simp argument is unused:
← hsw_lvl
Hint: Omit it from the simp argument list.
simp only [← hne_lvl, ← hsw̵_̵l̵v̵l̵,̵ ̵←̵ ̵h̵s̵e_lvl] at hb
Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Conway/Life/JumpCapture.lean:534:36: Variable name `hT` is not explicitly referenced.
The binding can be removed (if unused) or named `_` (if used implicitly).
Note: This linter can be disabled with `set_option linter.unusedVariables false`
Build completed successfully (8733 jobs).
Exit code : 0
SUCCESS : le module Conway compile (preuves valides, 0 sorry).
On confirme par un scan sorry global sur le module (en excluant les faux positifs en commentaires) : le corpus Conway des 5 noix ci-dessus est a 0 sorry réel.
# Scan global sorry reels sur les 5 noix (filtre les doc-comments)targets = ['Conway/DoomsdayLemmas.lean', 'Conway/LookAndSayLemmas.lean','Conway/Nim.lean', 'Conway/Angel.lean', 'Conway/Life.lean',]total =0for t in targets: s = count_real_sorry((WIN_LEAN_PROJECT / t).read_text(encoding='utf-8')) total += sprint(f" {t:<36} sorry reels = {s}")print("-"*50)print(f"TOTAL sorry reels sur les 5 noix : {total}")assert total ==0, "Regression : un sorry reel est apparu dans le corpus Conway !"print("OK - les 5 noix sont intégralement prouvées.")
Conway/DoomsdayLemmas.lean sorry reels = 0
Conway/LookAndSayLemmas.lean sorry reels = 0
Conway/Nim.lean sorry reels = 0
Conway/Angel.lean sorry reels = 0
Conway/Life.lean sorry reels = 0
--------------------------------------------------
TOTAL sorry reels sur les 5 noix : 0
OK - les 5 noix sont intégralement prouvées.
3.7 Calcul vivant : #eval en direct
On exécute en direct quelques #eval Lean (depuis un petit script qui importe les modules compiles), pour voir les calculs : le nim-sum de [3,4,5], le verdict gagnant/perdant, et le cardinal du moveset de l’Ange. (Necessite que le build précédent ait réussi ; sinon, message explicite.)
# Demonstration live de #eval via `lake env lean` sur un script ephemeredemo =r"""import Conway.Nimimport Conway.Angelopen Conway#eval s!"nimSum [3,4,5] = {nimSum [3,4,5]}"#eval s!"isWinningNim [3,4,5] = {isWinningNim [3,4,5]}"#eval s!"isWinningNim [1,1] = {isWinningNim [1,1]}"#eval s!"angelMoves card k=1 (roi) = {(angelMoves 1 (0,0)).card}"#eval s!"angelMoves card k=2 = {(angelMoves 2 (0,0)).card}""""# Ecrit le script dans /tmp (WSL) et l'exécute dans l'environnement du projet.# Note : un `lean` frais recharge tous les oleans (mathlib inclus) depuis le# système de fichiers monte (lecture lente) -> compter ~6 min meme build chaud.script_b64 = demo.encode('utf-8').hex()cmd = (f'source ~/.elan/env 2>/dev/null; cd {LEAN_PROJECT} && 'f'python3 -c "import sys,binascii; open(\'/tmp/conway_demo.lean\',\'wb\').write(binascii.unhexlify(sys.argv[1]))" {script_b64} && 'f'lake env lean /tmp/conway_demo.lean 2>&1')rc, out, err = wsl(cmd, timeout=600)print(out.strip() if out.strip() else'(pas de sortie)')print()if rc ==0:print("SUCCESS : calculs Lean exécutés en direct (les définitions réelles tournent).")elif rc ==-1:print("TIMEOUT (>600s) : chargement des oleans trop lent sur ce FS ; la cellule `lake build Conway` ci-dessus reste la preuve que les 5 .lean compilent.")else:print(f"Exit code {rc}.")if err.strip():print('STDERR:', err[-300:])
3.8 Conway dans Mathlib : le satellite Conway/MathlibMap.lean
Le module satellite Conway/MathlibMap.lean recense ce que Mathlib fournit réellement (pour la version pinnee du projet) en rapport avec les contributions de Conway. Il contient des #check qui attestent que ces définitions compilent, et une note historique documentant les modules de théorie des jeux combinatoires (Surreal, PGame, Nim, Nimber) qui furent present dans Mathlib puis retires en fevrier 2026 (PR #35550).
Trois domaines Conway-adjacents survivent dans Mathlib :
Arithmetique ordinale (Ordinal.instPow, Ordinal.CNF.rec, Ordinal.log) — le socle des “jours de naissance” des surreels.
Groupes de Coxeter (CoxeterMatrix, CoxeterSystem, CoxeterSystem.simple, CoxeterSystem.lift) — les symetries que Conway exploitait pour le reseau de Leech et l’Atlas.
Addition de jeux (Prod.GameAdd, WellFounded.prod_gameAdd) — la relation abstraite qui modelise la somme de deux jeux combinatoires, residu de la théorie de Sprague-Grundy.
Pour les domaines centraux de Conway (nombres surreels, jeux partisans, Sprague-Grundy), le depot vihdzp/combinatorial-games fournit la formalisation de reference. Importe comme dépendance Lake dans notre projet conway_cgt_lean/ (pattern Peters), il est presente en section 3.9 ci-dessous.
# Lecture du satellite MathlibMap.lean (single source of truth)print("=== Conway/MathlibMap.lean ===")print()# MathlibMap contient des #check (pas des theorem/def), on les extrait directementimport remm_text = (WIN_LEAN_PROJECT /'Conway/MathlibMap.lean').read_text(encoding='utf-8')check_re = re.compile(r'^\s*#check\s+(.+)', re.MULTILINE)decl_re = re.compile(r'^\s*(theorem|lemma|def|abbrev|instance)\s+([\w\'À-ſ]+)')sorry_count = count_real_sorry(mm_text)checks = check_re.findall(mm_text)decls = decl_re.findall(mm_text)print(f" {len(mm_text.splitlines())} lignes, sorry reels = {sorry_count}")print(f" {len(checks)} declarations #check (Mathlib showcase)")print(f" {len(decls)} declarations theorem/def")print()for i, c inenumerate(checks, 1):print(f" #{i} #check {c.strip()}")print()print("Note : les #check ci-dessus attestent que ces types existent dans la version")print("Mathlib pinnee (54f98fd6, mai 2026). Les modules Surreal/PGame/Nim/Nimber")print("ont ete retires de Mathlib en fevrier 2026 (PR #35550).")
=== Conway/MathlibMap.lean ===
120 lignes, sorry reels = 0
10 declarations #check (Mathlib showcase)
0 declarations theorem/def
#1 #check @Ordinal.instPow
#2 #check @Ordinal.CNF.rec
#3 #check @Ordinal.log
#4 #check @CoxeterMatrix
#5 #check @CoxeterMatrix.Group
#6 #check @CoxeterSystem
#7 #check @CoxeterSystem.simple
#8 #check @CoxeterSystem.lift
#9 #check @Prod.GameAdd
#10 #check @WellFounded.prod_gameAdd
Note : les #check ci-dessus attestent que ces types existent dans la version
Mathlib pinnee (54f98fd6, mai 2026). Les modules Surreal/PGame/Nim/Nimber
ont ete retires de Mathlib en fevrier 2026 (PR #35550).
3.9 Théorie des jeux combinatoires : conway_cgt_lean/CGTTour.lean
Les modules centraux de Conway — nombres surreels, jeux combinatoires, nimbers — ne sont plus dans Mathlib depuis fevrier 2026 (PR #35550). Ils ont ete relocalises et considerablement enrichis dans le depot vihdzp/combinatorial-games par la même auteure (Violeta Hernandez Palacios, vihdzp).
Suivant le pattern Peters (cf. social_choice_lean_peters/), nous importons ce depot comme dépendance Lake sans dupliquer son code, et nous presentons ses résultats cles via le module CGTTour.lean. Ce second projet Lake (conway_cgt_lean/, toolchain v4.31.0-rc2) est indépendant de conway_lean/ (v4.33.0).
Résultats formalises (13 #check) :
Domaine
Résultat
#check
Jeux
Quotient IGame -> Game
@Game.mk
Jeux
Groupe abélien ordonné
AddCommGroupWithOne Game
Jeux
Ordre partiel
PartialOrder Game
Surreels
Construction
@Surreal.mk
Surreels
Ordre linéaire
LinearOrder Surreal
Surreels
Théorème de simplicite
IGame.Fits.equiv_of_forall_not_fits
Surreels
Anneau commutatif
CommRing Surreal
Surreels
Embedding dyadiques
Dyadic.toIGame
Surreels
Embedding ordinaux
NatOrdinal.toSurreal
Nimbers
Addition nim (mex)
Nimber.add_def
Nimbers
Converse mex
Nimber.exists_of_lt_add
Nimbers
Corps de caractéristique 2
Field Nimber
# Lecture du module CGTTour.lean (projet conway_cgt_lean, pattern Peters)# Ce projet est dans GameTheory/ (autre repertoire que conway_lean/)def find_cgt_project():"""Auto-detecte conway_cgt_lean/ depuis le notebook.""" current = Path.cwd()for _ inrange(8): candidate = current /'conway_cgt_lean'if candidate.exists() and (candidate /'lakefile.lean').exists():return candidate gt_dir = current /'MyIA.AI.Notebooks'/'GameTheory' candidate = gt_dir /'conway_cgt_lean'if candidate.exists() and (candidate /'lakefile.lean').exists():return candidate current = current.parentreturnNoneCGT_PROJECT_WIN = find_cgt_project()if CGT_PROJECT_WIN: CGT_PROJECT_WSL = win_to_wsl(CGT_PROJECT_WIN) cgt_text = (CGT_PROJECT_WIN /'CGTTour.lean').read_text(encoding='utf-8') cgt_sorry = count_real_sorry(cgt_text)# Extract #check statements check_re_cgt = re.compile(r'^\s*#check\s+(.+)', re.MULTILINE) checks_cgt = check_re_cgt.findall(cgt_text)print(f"=== conway_cgt_lean/CGTTour.lean ({len(cgt_text.splitlines())} lignes, sorry = {cgt_sorry}) ===")print(f"Projet Lean (WSL) : {CGT_PROJECT_WSL}")print(f"Toolchain : {(CGT_PROJECT_WIN /'lean-toolchain').read_text(encoding='utf-8').strip()}")print(f"Dependance : vihdzp/combinatorial-games (Apache-2.0)")print()for i, c inenumerate(checks_cgt, 1):print(f" #{i:>2} #check {c.strip()}")print()print(f"Total : {len(checks_cgt)} declarations #check, {cgt_sorry} sorry.")print("Source unique de verite : le depot importe, pas duplique.")else:print("conway_cgt_lean/ non trouve (projet CGT independant)") CGT_PROJECT_WSL =None
=== conway_cgt_lean/CGTTour.lean (173 lignes, sorry = 0) ===
Projet Lean (WSL) : <repo>MyIA.AI.Notebooks/GameTheory/conway_cgt_lean
Toolchain : leanprover/lean4:v4.31.0-rc2
Dependance : vihdzp/combinatorial-games (Apache-2.0)
# 1 #check @Game.mk -- IGame → Game (application du quotient)
# 2 #check (inferInstance : AddCommGroupWithOne Game)
# 3 #check (inferInstance : PartialOrder Game)
# 4 #check @Surreal.mk -- IGame → [Numeric] → Surreal
# 5 #check (inferInstance : LinearOrder Surreal) -- Ordre total sur les surréels
# 6 #check @IGame.Fits.equiv_of_forall_not_fits -- Théorème de simplicité
# 7 #check (inferInstance : CommRing Surreal)
# 8 #check (inferInstance : LinearOrder Surreal)
# 9 #check @Dyadic.toIGame -- Plongement Rationnel dyadique → IGame
#10 #check @NatOrdinal.toSurreal -- NatOrdinal ↪o Surreal
#11 #check @Nimber.add_def -- Définition de l'addition de nim par mex
#12 #check @Nimber.exists_of_lt_add -- Réciproque : toute valeur plus petite est atteinte
#13 #check (inferInstance : Field Nimber)
Total : 13 declarations #check, 0 sorry.
Source unique de verite : le depot importe, pas duplique.
# Build du module CGTTour (projet independant, toolchain v4.31.0-rc1)if CGT_PROJECT_WIN:print(f"Lancement de `lake build CGTTour` via WSL (timeout 1500s)...")print(f"Projet : {CGT_PROJECT_WSL}")print("-"*60) rc, out, err = wsl(f'source ~/.elan/env 2>/dev/null; cd {CGT_PROJECT_WSL} && lake build CGTTour 2>&1 | tail -20', timeout=1500, )print(out)if err and err.strip() andnot err.strip().startswith('TIMEOUT'):print('STDERR:', err[-300:])print()print(f"Exit code : {rc}")if rc ==0:print("SUCCESS : CGTTour compile (12 #check verifies, 0 sorry).")print("Le depot vihdzp/combinatorial-games fournit la formalisation de reference")print("des nombres surreels, jeux combinatoires et nimbers.")elif rc ==-1:print("TIMEOUT : build a froid trop long ici ; la verification CI/PR est autoritative.")else:print("Voir le log ci-dessus.")else:print("Build saute : projet conway_cgt_lean/ non detecte.")
Lancement de `lake build CGTTour` via WSL (timeout 1500s)...
Projet : <repo>MyIA.AI.Notebooks/GameTheory/conway_cgt_lean
------------------------------------------------------------
Exit code : -1
TIMEOUT : build a froid trop long ici ; la verification CI/PR est autoritative.
4. Exercices
Trois exercices pour s’approprier les “noix” de Conway. Completer les stubs # TODO. Le notebook s’exécute de bout en bout même si les exercices ne sont pas completes (les cellules ne levent jamais d’erreur).
Exercice 1 - nim-sum et stratégie gagnante
Implementer en Python le nim-sum (XOR de tous les tas) et en deduire si la position est gagnante pour le joueur au trait (gagnante ssi nim-sum != 0). Comparer avec le théorème Lean isWinningNim_345 (isWinningNim [3,4,5] = true).
Indice : ^ est l’opérateur XOR en Python ; functools.reduce parcourt la liste.
from functools importreducedef nim_sum(heaps):"""Retourne le XOR de tous les tas. TODO étudiant."""# TODO: calculer le nim-sum (XOR de tous les éléments de heaps)# Indice : reduce(lambda a, b: a ^ b, heaps, 0)returnNone# TODO etudiantdef is_winning_nim(heaps):"""True si la position est gagnante pour le joueur au trait. TODO étudiant."""# TODO: gagnante ssi nim_sum(heaps) != 0returnNone# TODO etudiant# Vérification attendue (cf. théorème Lean isWinningNim_345) :# nim_sum([3,4,5]) == 2 et is_winning_nim([3,4,5]) == Trueprint("Exercice 1 a completer : nim_sum([3,4,5]) =", nim_sum([3, 4, 5]))print(" is_winning_nim([3,4,5]) =", is_winning_nim([3, 4, 5]))
Generer la suite “look-and-say” : a partir d’un terme, lire les groupes de chiffres identiques et ecrire “comptage puis chiffre”. Exemple : 1211 se lit “un 1, un 2, deux 1” -> 111221. Comparer le 5e terme avec ce que produit la formalisation Lean (lookAndSay 4 = 111221).
Indice : itertools.groupby regroupe les caractères consécutifs identiques.
from itertools import groupbydef look_and_say_next(s: str) ->str:"""Retourne le terme suivant de la suite look-and-say a partir de la chaine s. TODO étudiant."""# TODO: pour chaque groupe de chiffres identiques, concatener str(len(groupe)) + chiffre# Indice : "".join(f"{len(list(g))}{ch}" for ch, g in groupby(s))returnNone# TODO etudiant# Vérification attendue : en partant de "1", les premiers termes sont# 1 -> 11 -> 21 -> 1211 -> 111221 (cf. théorème Lean lookAndSay_4 = 111221)terme ="1"print("Exercice 2 a completer - suite look-and-say :")for i inrange(5):print(f" terme {i}: {terme}") nxt = look_and_say_next(terme)if nxt isNone:print(" (a completer)")break terme = nxt
Exercice 2 a completer - suite look-and-say :
terme 0: 1
(a completer)
Exercice 3 - cardinal du moveset de l’Ange
L’Ange de puissance \(k\) atteint toutes les cases a distance de Chebyshev \(\leq k\), sauf sa position courante : soit un carré \((2k+1)\times(2k+1)\) prive de son centre, donc \((2k+1)^2 - 1\) cases. Implementer ce comptage et vérifier contre les théorèmes Lean kingMoves_card (\(k=1 \to 8\)) et angelMoves2_card (\(k=2 \to 24\)).
Indice : pas besoin d’enumerer les cases, la formule fermee suffit.
def angel_moves_card(k: int) ->int:"""Nombre de cases atteignables par un Ange de puissance k. TODO etudiant."""# TODO: retourner (2*k + 1)**2 - 1returnNone# TODO etudiant# Vérification attendue (cf. théorèmes Lean) :# angel_moves_card(1) == 8 (kingMoves_card)# angel_moves_card(2) == 24 (angelMoves2_card)for k in (1, 2, 3):print(f"Exercice 3 a completer : angel_moves_card({k}) = {angel_moves_card(k)}")
Exercice 3 a completer : angel_moves_card(1) = None
Exercice 3 a completer : angel_moves_card(2) = None
Exercice 3 a completer : angel_moves_card(3) = None
Conclusion
Conway laisse une oeuvre dont la profondeur dépasse de loin sa vitrine grand public. Des nombres surreels aux groupes sporadiques, du reseau de Leech au Monstrous Moonshine, de la théorie des noeuds (le noeud qui porte son nom, tranche en 2020) a l’empilement de spheres, du 15-théorème en théorie des nombres aux pavages (critere de Conway et notation orbifold), son genie a consiste a voir de la structure mathematique serieuse la ou les autres ne voyaient que des jeux.
Ce notebook a parcouru ce panorama puis exécute les preuves Lean réelles de cinq de ses “noix” : Doomsday, Look-and-Say, Nim, le problème de l’Ange, et les fondations du Jeu de la Vie — toutes a 0 sorry, compilees depuis le depot. Il presente également le tour de la théorie des jeux combinatoires (nombres surreels, nimbers, théorème de simplicite) importe depuis vihdzp/combinatorial-games via le projet conway_cgt_lean/.
Pour aller plus loin
Lean-16b : le Jeu de la Vie comme modèle de calcul (Hashlife, RLE, spaceships, computation universelle).