Gorard #19741 — greffe lot Serre100 (06 + 10)

MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/06-bulles-minkowski.ipynb

@@ -595,7 +595,13 @@
     "tags": []
    },
    "source": [
-    "**Lecture** : la colonne « rapport » croît brutalement — E8 est 32× au-dessus de la borne, Leech 16 000×. Le message contre-intuitif de la haute dimension : **on ne sait même pas construire explicitement** un réseau approchant Minkowski-Hlawka, alors que la nature (E8, Leech) fournit des solutions parfaites. C'est le contour exact du paysage que Hlawka, Minkowski et leurs héritiers ont tracé — et où la théorie des nombres moderne, celle de Serre, puise ses constantes."
+    "**Lecture** : la colonne « rapport » croît brutalement — E8 est 32× au-dessus de la borne, Leech 16 000×. Le message contre-intuitif de la haute dimension : **on ne sait même pas construire explicitement** un réseau approchant Minkowski-Hlawka, alors que la nature (E8, Leech) fournit des solutions parfaites. C'est le contour exact du paysage que Hlawka, Minkowski et leurs héritiers ont tracé — et où la théorie des nombres moderne, celle de Serre, puise ses constantes.\n",
+    "\n",
+    "> *« The timelines were completely wrong. I was scared on a very personal level. We're not putting the genie back in the bottle. »* -- J. Gorard, *The Physicist Revolutionizing Physics With AI* (Theories of Everything, 2026, [00:00])\n",
+    ">\n",
+    "> *« We want to make physics executable in the same way that software is executable. »* -- *ibid.*, [00:24] -- la thèse de Lanyon AI, la société que Gorard vient de fonder, énoncée dès la première minute de l'entretien.\n",
+    "\n",
+    "**Le pont avec ce carnet est une analogie, et elle vaut d'être explicite** : « exécutable » veut dire *constructible*, pas seulement *énonçable*. Or le tableau ci-dessus mesure précisément cet écart -- la borne de Minkowski-Hlawka s'énonce et se calcule en une ligne, mais aucun réseau approchant ne se construit explicitement, tandis qu'E8 et Leech existent sans qu'on ait eu à les chercher. Le carnet ne comble pas cet écart : il le rend visible. C'est la version géométrique de la question que l'entretien pose à la physique."
    ]
   },
   {

MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/10-empilements-borne-lp-cohn-elkies.ipynb

@@ -429,7 +429,13 @@
     "- de même $\\widehat f(s_j) \\ge \\sum_i u_i\\, v^s_{ij}$ couvre le demi-axe positif de $\\widehat f$ ;\n",
     "- les **queues** au-delà des grilles : chaque $g_i$ décroît, donc $|f(x) - f(t_{\\max})| \\le \\sum_i u_i\\, g_i(t_{\\max})$ pour $x \\ge t_{\\max}$ — la contrainte $f(t_{\\max}) \\le -\\sum_i u_i\\, g_i(t_{\\max})$ ferme $[t_{\\max}, \\infty[$, et symétriquement pour $\\widehat f$.\n",
     "\n",
-    "Tout reste **linéaire** en $(p, n)$ : c'est encore un LP, mais dont chaque solution est un certificat *a posteriori vérifiable* — la cellule d'après le vérifie sur grille dense."
+    "Tout reste **linéaire** en $(p, n)$ : c'est encore un LP, mais dont chaque solution est un certificat *a posteriori vérifiable* — la cellule d'après le vérifie sur grille dense.\n",
+    "\n",
+    "**Pourquoi « certifier » est le mot juste.** La section vient de remplacer « je l'ai vérifié » par un objet que d'autres peuvent re-vérifier : des contraintes par intervalle, et des queues fermées. L'entretien de Gorard donne à ce geste son échelle industrielle :\n",
+    "\n",
+    "> *« And then in March, 2026, there was this big, you know, auto formalized proof dropped by this, this startup math, Inc. »* -- J. Gorard, *The Physicist Revolutionizing Physics With AI* (Theories of Everything, 2026, [01:54]) -- suivi, quelques secondes plus loin, de la précision qui compte : *« Completely done autonomously, end to end, using effectively an AI harness. »* ([02:12]). Gorard, qui travaillait sur la démonstration automatique depuis une dizaine d'années, en fait le déclencheur de son propre changement de jugement.\n",
+    "\n",
+    "La différence de nature avec ce carnet mérite d'être nommée, parce qu'elle est facile à confondre : ici, un **solveur LP** produit une solution dont l'admissibilité se vérifie *a posteriori* sur des intervalles fermés ; une preuve auto-formalisée, elle, est **vérifiée par un noyau** qui n'accorde aucune confiance au producteur. Les deux remplacent la même chose -- la confiance envers l'auteur -- par un objet re-vérifiable. Le premier pas est celui de ce carnet ; le second est celui qui a changé l'avis de Gorard."
    ]
   },
   {
@@ -750,7 +756,13 @@
     "\n",
     "Le raffinement $K \\to 100$ fait converger les bornes vers $1{,}055$, $1{,}038$, $0{,}987$ — lentement : le plafond du dictionnaire gaussien certifié reste loin des valeurs de Cohn–Elkies 2003 (traits pointillés : $0{,}9998$ et $0{,}7796$, obtenues par une discrétisation en polynômes de Laguerre, propres de la transformée de Fourier, sans garantie d'intervalle fermée). Notre méthode démontre *moins* — mais elle démontre : chaque nombre du tableau ci-dessus est appuyé sur un certificat vérifié à la cellule précédente.\n",
     "\n",
-    "**Et en dimensions 8 et 24 ?** Le même théorème y devient *exact* : Viazovska (2016) construit des fonctions admissibles dont la borne vaut exactement la densité de $E_8$, $\\pi^4/384 \\approx 0{,}2537$ — puis avec Cohn, Kumar, Miller, Radchenko, celle du réseau de Leech, $\\pi^{12}/12! \\approx 0{,}001930$. Ces fonctions ne sont pas dans le dictionnaire des Gaussiennes : ce sont des **intégrales de formes modulaires** $E_4$, $E_6$ interpolées — la famille du $\\Delta = \\eta^{24}$ du carnet 09. Techniquement, exiger $\\widehat f \\ge 0$ *partout* (et non plus sur un maillage) transforme le LP en problème de programmation semi-définie (SDP) : c'est le saut de 2016, et la réponse à la conjecture que Cohn–Elkies formulaient explicitement pour les dimensions 8 et 24. La boucle du carnet 09 se referme : les formes modulaires qui portaient la lacunarité de $\\eta^r$ portent aussi l'optimalité des empilements."
+    "**Et en dimensions 8 et 24 ?** Le même théorème y devient *exact* : Viazovska (2016) construit des fonctions admissibles dont la borne vaut exactement la densité de $E_8$, $\\pi^4/384 \\approx 0{,}2537$ — puis avec Cohn, Kumar, Miller, Radchenko, celle du réseau de Leech, $\\pi^{12}/12! \\approx 0{,}001930$. Ces fonctions ne sont pas dans le dictionnaire des Gaussiennes : ce sont des **intégrales de formes modulaires** $E_4$, $E_6$ interpolées — la famille du $\\Delta = \\eta^{24}$ du carnet 09. Techniquement, exiger $\\widehat f \\ge 0$ *partout* (et non plus sur un maillage) transforme le LP en problème de programmation semi-définie (SDP) : c'est le saut de 2016, et la réponse à la conjecture que Cohn–Elkies formulaient explicitement pour les dimensions 8 et 24. La boucle du carnet 09 se referme : les formes modulaires qui portaient la lacunarité de $\\eta^r$ portent aussi l'optimalité des empilements.\n",
+    "\n",
+    "**Le même résultat, vu de l'entretien.** Jonathan Gorard date de mars 2026 le basculement de son propre jugement sur l'IA, et le cas qu'il cite est exactement le sujet de cette section :\n",
+    "\n",
+    "> *« ... the Marina Vyazovska, like eight and 24 dimensional sphere packing problem that she won the field medal for. »* -- J. Gorard, *The Physicist Revolutionizing Physics With AI* (Theories of Everything, 2026, [02:04]) -- Maryna Viazovska a reçu la médaille Fields en 2022 pour le cas $n = 8$. Ce que la borne du carnet approche par un LP certifié, la preuve de 2016 l'établit **exactement** : la fonction admissible optimale y est explicite, et elle s'écrit avec les formes modulaires du carnet 09.\n",
+    "\n",
+    "L'écart mesuré plus haut -- $1{,}055$ certifié contre $0{,}9998$ -- ne sépare donc pas une méthode fausse d'une méthode juste, mais deux sens du mot *démontrer* : **certifier** sur une grille fermée, et **atteindre l'optimum**. En dimension 8, la frontière se referme : la fonction admissible optimale est connue, explicite, et sa borne vaut exactement la densité de $E_8$."
    ]
   },
   {