Ré-étude de la preuve formelle — audit SOTA (2026-07-08)

Tâche task-20260708-dd32. Mathlib pin EFS : leanprover/lean4:v4.29.0. Registre : forensique. Toute affirmation est adossée à un fichier:ligne, une URL, ou un hash de commit.

Mandat opérateur. Question posée : « des sorry ont-ils sauté grâce à des progrès amont (Mathlib, Armstrong–Kempe) ? » Puis, pour chacun des 4 sorry restants, statuer — fermable-maintenant / fermable-avec-DeGiorgi-import / toujours-research-grade — avec un plan chiffré, en évaluant deux candidats SOTA nouveaux : (a) le dépôt Lean scottnarmstrong/DeGiorgi (De Giorgi–Nash–Moser elliptique, arXiv 2604.05984), (b) Mathlib HEAD post-v4.29.0.

0. Verdict en une image

Deux choses ont été confondues dans la question, et il faut les séparer nettement :

• Est-ce l'amont qui a fermé les sorry ? → NON. Le compteur est passé de 6 → 4 entre juin et juillet 2026, mais aucun octet de Mathlib n'a bougé : le pin est resté v4.29.0 figé depuis le 17 avril 2026. Les fermetures sont toutes des commits de la flotte locale (M1, Heat, Widder). L'amont n'a rien offert ; c'est la maison qui a bâti les briques.

• L'amont nouveau de juillet peut-il fermer les 4 restants ? → NON, pour les deux candidats. Le dépôt DeGiorgi est elliptique (régularité de solutions faibles à coefficients mesurables) là où nos obligations sont paraboliques et classiques (principe de comparaison sur des solutions C² à coefficient constant Δ) : mauvais registre, pas seulement mauvaise équation. Mathlib HEAD (aujourd'hui ≈ v4.31) n'a fait atterrir aucune théorie parabolique, aucun principe du maximum, aucune unicité Widder/Tychonoff depuis v4.29.0.

• Mais l'un des 4 sorry — gaussian_conv_solves_heat (brique M2) — est fermable-maintenant par assemblage Mathlib pur, sans aucun apport SOTA. Il l'était déjà ; le SOTA ne change rien à ce constat, il le confirme. Une molécule de fermeture peut être nucléée (cf. §5). Cette tâche ne la fait pas.

1. Réponse forensique : l'amont n'a fermé aucun sorry

1.1 Le pin Mathlib n'a jamais bougé

$ git log -1 --format='%H %ci' -- lean/EFS/lakefile.toml
decd110c0e458d527c7a1c2f51d97a37e734820c 2026-04-17 01:38:37 +0200

Le fichier qui déclare la dépendance Mathlib (lean/EFS/lakefile.toml, rev = "v4.29.0") n'a été touché qu'une seule fois — au bootstrap du projet Lake, le 17 avril 2026 (decd110). Idem pour lean-toolchain (leanprover/lean4:v4.29.0). Il est donc impossible qu'un progrès Mathlib ait fermé quoi que ce soit : le tree Mathlib vu par EFS est gelé à la SHA 8a178386ffc0f5fef0b77738bb5449d50efeea95 (= tag v4.29.0, cf. docs/lore/lean-unproved.md §1).

1.2 Les 6 → 4 sont des commits locaux, datés, nommés

Les trois hashes existent dans l'historique (git log --oneline les résout). Le compteur sorry global : 6 (post-S1) → 4 après 2dee9c6 (ferme 2 sous-sorry Heat) — cf. docs/lore/lean-unproved.md, section Pipeline (« Total sorry count = 4 (was 6 ; task-20260707-ddc7 closed two) »).

Conclusion §1. Aucun sorry n'a « sauté grâce à l'amont ». La question de l'opérateur reçoit un NON forensiquement clos : pin gelé + fermetures locales tracées.

2. Recensement des 4 sorry restants

Grep des obligations vives (les sorry du corpus adverse EFS/Adversarial/** — TypeUniverseMismatch:27, DegeneratePhi:33 — sont des sites d'échec voulus, garde duale, hors décompte) :

$ grep -rn '^  sorry$\|^    sorry$' EFS/Heat.lean EFS/Q3.lean EFS/Q3/Widder.lean
EFS/Heat.lean:275
EFS/Q3/Widder.lean:198
EFS/Q3.lean:509
EFS/Q3.lean:531

Les 4 se réduisent à deux racines feuilles : S1 (existence/heat, faisable) et S2 (unicité parabolique, research-grade). S3 et S4 sont du câblage : ils tombent dès que leur racine tombe (plus leur propre glue, mineure — S3 = chaîne de dérivation Cole–Hopf déjà prouvée en M1 ; S4 = density_path_unique_of_heat, déjà prouvé modulo S2).

Détail mathématique de chaque racine (source de vérité : EFS/Heat.lean docstring l.229–268 pour S1 ; EFS/Q3/Widder.lean docstring l.158–186 + docs/research/widder-attempt.md pour S2) :

• S1 — pousser ∂_t et Δ_x sous l'intégrale de convolution (p ⋆ K_t). Les deux sous-lemmes durs sont déjà fermés (heatKernel_solves_heat, integrable_heatKernel, 0 sorry / 0 axiome, 2dee9c6). Ce qui reste est la dérivation dominée : hasDerivAt_integral_of_dominated_loc_of_deriv_le avec une borne gaussienne uniforme. Revue de faisabilité von-Neumann (task-20260707-ddc7) : le théorème est VRAI et prouvable tel quel ; l'hypothèse porteuse est hp_int (p ∈ L¹), la domination passe par L¹ seul. Le seul frein : tout lemme de convolution-différentiation de Mathlib v4.29.0 exige un support compact d'un facteur, que le noyau gaussien n'a pas — d'où un assemblage main de plusieurs centaines de lignes (candidat Mathlib.Analysis.PDE.Heat).

• S2 — unicité sous-gaussienne (Tychonoff 1935) via le principe du maximum parabolique faible sur cylindres bornés (0,T]×B_R + barrière Tychonoff–Täcklind quand R → ∞. Demi-spatial déjà prouvé (EFS.HJ.laplacian_nonpos_of_isLocalMax, 0 sorry). Reste absent de Mathlib v4.29.0 : (T) le signe de la dérivée temporelle unilatérale au maximum espace-temps (+ case-split intérieur/bord parabolique), (B) la barrière gaussienne localisante. Cf. docs/research/widder-attempt.md §3.

3. Les deux candidats SOTA nouveaux (juillet 2026)

3a. Le dépôt Armstrong–Kempe DeGiorgi

Fiche signalétique (sources ci-dessous) :

Viabilité d'un import Lake — les feux techniques sont au vert :

1. Licence : Apache 2.0 = exactement celle d'EFS (cf. en-têtes EFS/*.lean : « Released under Apache 2.0 license »). ✅ Aucun frein juridique.
2. Toolchain : DeGiorgi = v4.29.0-rc6, EFS = v4.29.0 (release finale). Même minor ; rc6 est le dernier candidat avant le tag final. ✅ Compatible.
3. Nuance de pin Mathlib : DeGiorgi pointe la rev 5c8398d (rc6), EFS la 8a17838 (v4.29.0 final) — deux commits distincts (quelques commits d'écart). Lake impose une seule version de Mathlib sur tout le graphe de dépendances ; un import réel demanderait donc de rebaser DeGiorgi sur le v4.29.0 final (ou bumper EFS sur rc6). Delta faible, risque faible — mais non nul. ⚠️ Réconciliation de pin nécessaire.

Verdict mathématique — l'import ne ferme aucun des 4 sorry :

Le point dur n'est pas la plomberie mais le registre. De Giorgi–Nash–Moser répond à « une solution faible à coefficients mesurables est-elle régulière ? » (Hölder, Harnack). Nos obligations demandent « une solution classique C² à coefficient constant Δ est-elle unique dans la classe de Tychonoff ? » — une question de comparaison/ordre, pas de régularité. Concrètement :

• S2 (le seul candidat plausible pour DeGiorgi) — le principe du maximum parabolique faible dont on a besoin est plus élémentaire que De Giorgi : c'est un case-split ponctuel au maximum espace-temps (calcul, pas d'espaces de Sobolev). Le dépôt ne contient aucun principe du maximum, et sa machinerie (Sobolev sur domaines bornés, Poincaré, John–Nirenberg, itération de Moser) est elliptique — pas de variable temps, pas de bord parabolique, pas de barrière Tychonoff–Täcklind. Même la Harnack qu'il fournit est elliptique ; et la parabolique de Moser (qu'il n'a pas) ne donnerait toujours pas l'unicité Tychonoff, qui repose sur la comparaison à une super-solution, non sur Harnack. → N'aide pas S2.
• S1 — pure question L¹ + dérivation dominée ; rien à voir avec la régularité elliptique. → N'aide pas S1.
• S3/S4 — câblage sur S1/S2. → N'aide pas.

Aucune des « primitives réutilisables » du dépôt (Sobolev sur domaines bornés, Poincaré) n'est sur le chemin critique : le principe du maximum classique et la barrière sont ponctuels, ils ne touchent ni Sobolev ni Poincaré.

Signal cosmon-ward (positif, non-bloquant). Le dépôt DeGiorgi est néanmoins la preuve d'existence qu'un chantier PDE lourd est formalisable à l'échelle en Lean, avec des blueprints + LLM (≈ 2 semaines, 56k lignes). Il valide la méthodologie (blueprint-driven autoformalization) que la brique S2 demanderait — sans en fournir la matière. À citer comme référence de méthode, pas comme dépendance.

3b. Mathlib HEAD post-v4.29.0

Ce qui a bougé en amont depuis le pin : Lean/Mathlib a publié v4.30.0 (2026-05-26), puis v4.31.0, avec v4.32.0-rc1 en vol (cf. releases Lean, releases Mathlib). EFS est resté sur v4.29.0. Il existe donc un amont neuf à auditer.

Ce qui a atterri d'utile (marginal pour nous) :

• InnerProductSpace.laplacianWithin / notation Δ[s] — Laplacien relatif à un ensemble — nouveau dans le module Mathlib.Analysis.InnerProductSpace.Laplacian (doc). Confort pour des domaines bornés, mais ce n'est pas un principe du maximum.
• HasDerivWithinAt.nonneg_of_monotoneOn (et le dual antitone) — signe de la dérivée unilatérale d'une fonction monotone sur un ensemble (Deriv.Slope). Potentiellement un ingrédient de la condition nécessaire d'extrémité (T), mais pas le scaffolding parabolique.

Ce qui n'a toujours pas atterri (vérifié sur la doc HEAD) :

• Aucun principe du maximum (le module Laplacien HEAD n'a aucun lemme « Δ ≤ 0 au max local » — c'est précisément pourquoi EFS a dû le prouver localement, laplacian_nonpos_of_isLocalMax).
• Aucune théorie parabolique / équation de la chaleur (existence de la solution fondamentale de Weierstrass, dérivation dominée sans support compact).
• Aucune unicité Widder 1944 / Tychonoff 1935.

Upgrade de pin envisageable ? Gain net ≈ nul pour la fermeture. Passer à v4.30/v4.31 apporterait Δ[s] et un lemme de dérivée unilatérale — de quoi raccourcir marginalement la brique S2 (le pas (T)), jamais de quoi fermer S1 ou S2. Le coût (rebaser tout l'appareil EFS.HJ.* et le corpus adverse de 23 entrées sur un nouveau tree Mathlib) dépasse le bénéfice. Recommandation : ne pas bumper le pin pour l'instant ; réévaluer si/quand une théorie parabolique atterrit réellement en amont (à surveiller sur le Zulip Mathlib/analysis).

4. Statut par sorry — verdict + plan chiffré

Résumé : 3 des 4 sorry sont sur le chemin fermable-maintenant (S1 en tête, puis S3, S4 en cascade), sans aucun apport DeGiorgi ni Mathlib-HEAD. Le seul irréductible reste S2 (unicité parabolique), et ni DeGiorgi ni Mathlib HEAD ne l'entament : c'est un chantier parabolique neuf, elliptique ≠ parabolique.

5. Y a-t-il un sorry devenu fermable-maintenant ? — OUI, explicitement

Oui : gaussian_conv_solves_heat (S1, EFS/Heat.lean:275) est fermable-maintenant. Précision honnête : il ne le devient pas grâce au SOTA de juillet — il l'était déjà (revue von-Neumann task-20260707-ddc7, « le théorème est VRAI et prouvable tel quel »). L'audit SOTA de cette tâche confirme ce statut et écarte l'illusion qu'un import DeGiorgi serait requis : la fermeture est un assemblage Mathlib v4.29.0 local, pas un blocage amont.

Dans la foulée, S3 (regularStable_to_admissible) devient fermable-maintenant modulo S1 — le sens direct de Q3 ne dépend que de S1 + M1 (déjà là).

Action (à nucléer séparément, PAS dans cette tâche — cf. mandat). Nucléer une molécule de fermeture ciblant S1 (gaussian_conv_solves_heat, dérivation dominée sous convolution gaussienne, ~200–400 lignes), puis en cascade S3. Bénéfice : sorry 4 → 2, et les 2 restants (S2 + S4) isolent proprement l'unique dette research-grade (l'unicité parabolique S2). Cette ré-étude n'exécute pas la fermeture (mandat : « si un sorry devient fermable, le dire — ne pas la faire soi-même »).

6. Signal cosmon-ward — la primitive manquante, inchangée

La primitive amont manquante identifiée de longue date (docs/lore/lean-unproved.md §6, docs/research/widder-attempt.md §3) reste debout et non payée par le SOTA de juillet :

Principe du maximum parabolique faible sur un cylindre borné + barrière Tychonoff–Täcklind — absent de Mathlib v4.29.0 et de Mathlib HEAD (v4.31). Le dépôt DeGiorgi, malgré ses 56k lignes de PDE elliptique, ne le fournit pas (mauvais registre : régularité elliptique ≠ comparaison parabolique). Le demi-spatial est payé localement (EFS.HJ.laplacian_nonpos_of_isLocalMax) ; restent (T) le signe temporel unilatéral au bord et (B) la barrière.

Aucune axiomatisation (règle galaxie « JAMAIS axiomatiser ») : le sorry unique garde l'obligation visible.

Sources

• Dépôt : github.com/scottnarmstrong/DeGiorgi — README (licence Apache 2.0), lean-toolchain (leanprover/lean4:v4.29.0-rc6), lake-manifest.json (mathlib rev 5c8398df528176d9c87ccd9226ba8f7c8852d59c).
• Article : arXiv:2604.05984 Formalization of De Giorgi–Nash–Moser Theory in Lean (Armstrong & Kempe, avril 2026).
• Billet : scottnarmstrong.com — Formalizing De Giorgi-Nash-Moser theory in Lean.
• Mathlib : doc InnerProductSpace.Laplacian, doc Deriv.Slope, releases Lean, releases Mathlib.
• Interne : lean/EFS/lakefile.toml (pin v4.29.0, dernier touché decd110 2026-04-17) ; commits 7b43b04 (M1), 2dee9c6 (Heat), 7562782 (Widder) ; EFS/Heat.lean:275, EFS/Q3/Widder.lean:198, EFS/Q3.lean:509, EFS/Q3.lean:531 ; docs/lore/lean-unproved.md, docs/research/widder-attempt.md, docs/research/autoformalization-sota.md.