Distiller 3SUM et APSP sous-cubiques : le word RAM formalisé (anthropics/formal-math) #23140

Part of #13106 -- demandée par le mainteneur le 2026-10-27 (Concern sur #22844 : « distiller les nouveaux résultats [...] Créer les issues dédiées »).

Contexte — ce que la source dit

anthropics/formal-math, projet 3sum-apsp/ : une formalisation Lean 4 qui accompagne l'article Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs de Josh Alman et Virginia Vassilevska Williams (arXiv:2610.06783v1).

README.md :

« This formalization accompanies the paper [...] It states results of the paper as theorems of Lean 4, in the paper's notation and numbering, and proves these theorems. »
« The five headline claims are stated in one self-contained file, EndStatement.lean. They are about programs of a word RAM, on Exact Triangle, 3SUM, the (min,+)-product, APSP and k-Clique. The file has 139 lines, imports nothing and contains no proof. For the five claims this one file is all that has to be read. »

Les cinq claims, tels que le README les tabule (exposants tels qu'imprimés) :

Le modèle, cité du README : « a word RAM with O(log n)-bit words » ; « There is no division, no shift, no bitwise operation, and no constant other than 1. » ; neuf types d'instructions, une par pas.

Ce que la source déclare non prouvé (README.md, section « What is not proved ») : les temps d'exécution sur entrées réelles et ceux de la section 5.1 ; et « The constants of the time bounds are not optimized; they are large, and for most theorems no value is given. »

Résonance mesurée avec le dépôt : MyIA.AI.Notebooks/Complexity/CARNET-NUMEROTATION.md et l'encart « gap Mathlib » de Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb constatent qu'aucune couche Computability/Complexity n'existe dans Mathlib — « pas de TIME(f) ». Or EndStatement.lean définit sa propre sémantique « résolu en temps O(n^r) » sur une machine nommée, dans le noyau Lean seul : c'est une réponse externe au trou que la série documente. Complexity-07c-LeBilanMathocalypse-Python.ipynb (14/10/2026) raconte déjà le résultat en prose et écrit : « aucun de ces résultats (UGC, L=BPL, parité ∉ QAC^0, exposants matmul/entiers, 3SUM sous-quadratique) n'a de formalisation référencée dans ce dépôt ». Cette phrase est datée de sa rédaction ; le présent projet la rend périmée pour le 3SUM.

Statut épistémique : énoncé formalisé par les auteurs (projet Palomar, Challenge/ + Solution/ + ThreeSumApsp/), non importé chez nous, non reconstruit par nous.

Ce qu'on en distille

Un carnet de la série Complexity, accrétion de la position 03, dont l'objet est le modèle de calcul, pas l'article :

• Cible : MyIA.AI.Notebooks/Complexity/Complexity-03e-Barrieres-Exposants-WordRAM-Python.ipynb. Lettre 03e attribuée par ai-01 le 2026-10-28 (CARNET-NUMEROTATION.md exclut tout résultat de recherche du chemin principal) ; 03d est le carnet frère sur l'ETH, portée par la même lane, qui livre 03d puis 03e.
• Contenu : (1) les cinq claims et leurs exposants ; (2) le word RAM de EndStatement.lean réimplémenté en Python — neuf instructions, comptage de pas — et vérifié sur une instance fermée dont le compte de pas est calculé à la main ; (3) le contrôle du scaling : le 3SUM quadratique mesuré sur les mêmes instances donne un exposant empirique ≈ 2, ce qui est un témoin du point de départ, jamais une mesure du gain annoncé ; (4) la leçon honnête : la borne est une borne d'existence de programme à constantes non optimisées, donc « 1,9992 » ne se mesure pas aujourd'hui.
• Non-duplication : le récit de la vague est dans Complexity-07c ; ce carnet ne le refait pas, il ajoute la surface machine-vérifiée et cite 07c comme récit. La correction de la phrase « aucune formalisation » de 07c se fait par une ligne de renvoi ajoutée dans 07c dans la même PR ou une PR sœur déclarée, pas par une réécriture du carnet.

Critères d'acceptation

• Avant toute rédaction, l'article arXiv:2610.06783v1 est archivé au gisement G:\Mon Drive\MyIA\IA\Bibliographie IA et lu ; le carnet n'attribue à l'article que ce qui est lu dans cette copie (bibliography-hygiene). Le corps de PR cite le dossier du gisement.
• Le carnet est sur main, toutes cellules de code exécutées avec sorties (execution_count non nul, C.2), zéro erreur, trois exercices C.1 non bloquants.
• Les cinq claims sont reproduits dans une table avec, pour chacun, le nom Lean (Theorem_19, Theorem_22_3SUM, Theorem_22_MinPlus, Theorem_22_APSP, Corollary_39_ZeroWeight), l'item de l'article et l'exposant tel qu'imprimé ; la source de chaque ligne est anthropics/formal-math/3sum-apsp/EndStatement.lean et README.md.
• L'interpréteur du word RAM est exécuté, et un témoin fermé est présent : sur une instance de taille fixée, le compte de pas rendu par l'interpréteur égale un compte calculé à la main dans une cellule markdown voisine. Le contrôle quadratique (exposant empirique ≈ 2) est présenté comme contrôle, avec la phrase explicite qu'il ne réfute rien.
• Une section « Ce que la source ne prouve pas » cite : les temps sur entrées réelles et la section 5.1 non prouvés ; les constantes non optimisées (« large, and for most theorems no value is given ») ; les opérations absentes de la machine (pas de division, pas de décalage, pas d'opération bit à bit, pas de constante autre que 1) ; et le fait que le claim est une existence de programme.
• La ligne du carnet est ajoutée à MyIA.AI.Notebooks/Complexity/README.md et CARNET-NUMEROTATION.md, la navigation est mise à jour, et la phrase de Complexity-07c sur l'absence de formalisation reçoit un renvoi daté (même PR ou PR sœur nommée dans le corps).

Sources

• anthropics/formal-math, projet 3sum-apsp : https://github.com/anthropics/formal-math/tree/main/3sum-apsp (README.md, EndStatement.lean, PaperStatements.lean, docs/MACHINE.md)
• Article formalisé : Alman et Vassilevska Williams, arXiv:2610.06783v1 (cité par le README du projet)
• Contexte dépôt : MyIA.AI.Notebooks/Complexity/Complexity-07c-LeBilanMathocalypse-Python.ipynb · Complexity-03b-HartmanisStearns-TimeHierarchy.ipynb · CARNET-NUMEROTATION.md