Gorard #19741 — greffe Lean-16a (épilogue 2.3b)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb

@@ -270,6 +270,19 @@
     "> *« 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."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "c7d1f2a9",
+   "metadata": {
+    "papermill": {},
+    "tags": []
+   },
+   "source": [
+    "### 2.3b Épilogue — la boucle formelle bouclée\n",
+    "\n",
+    "« the eight and 24 dimensional sphere packing problem that she won the field medal for » [2:04] : le problème que Viazovska a tranché en 2016 (ci-dessus) est exactement celui sur lequel l'entretien Gorard ouvre — une preuve d'empilement en dimension 8 **auto-formalisée et vérifiée par une machine** [1:58]. Le symétrique est parlant pour ce carnet : le résultat qui a valu une médaille Fields est devenu un théorème qu'un noyau vérifie seul. La frontière que les sections 3.x parcourent à la main sur des noix conwayennes (Doomsday, Nim, Life) s'est déplacée jusqu'aux preuves médaillées.\n"
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "7ad5638e",
@@ -2033,4 +2046,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}