Lean 8b : le programme Erdős et le pattern conjecture-as-sorry

Série : SymbolicAI / Lean — Digestions de résultats profonds, companion de Lean-08-Agentic-Proving-Python Navigation : Index | << Lean-08-Agentic-Proving-Python | Lean-09-SK-Multi-Agents-Lean-Python >>

Paul Erdős a laissé des centaines de problèmes ouverts, dotés en argent et suivis par une communauté ; la base erdosproblems.com (Thomas Bloom) les recense un par un, avec leur statut de formalisation Lean. Le projet Google DeepMind Formal Conjectures alimente ce mouvement et en a fait un benchmark de raisonnement automatique — cf. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics (arXiv:2605.13171, Firsching et al., 2026).

L’idée centrale tient en une phrase : une conjecture ouverte, formalisée en Lean, est un théorème au sorry près. Ce companion exécute ce pattern in-kernel, en côte à côte :

un théorème Erdős prouvé importé de Mathlib (Erdős–Ginzburg–Ziv) ;
une conjecture Erdős ouverte restatée à la main (équation d’Erdős–Moser) ;

et la commande #print axioms fait office de discriminant : le trio standard [propext, Classical.choice, Quot.sound] sans sorryAx d’un côté, sorryAx présent en plus de l’autre.

Vue d’ensemble

Un théorème prouvé, importé — EGZ : énoncé, signature Lean, axiomes.
Le témoin — EGZ appliqué sur un cas concret, témoin exhibé et vérifié.
Le pattern conjecture-as-sorry — Erdős–Moser restatée, sorryAx visible.
Provenance, attribution, dépendances — d’où vient chaque brique.
Friction et chemin de découverte — ce qui a résisté.
Exercices.

Environnement d’exécution

Notebook natif : kernel lean4-wsl-groth16200 (pattern per-lake), miroir WSL du lake grothendieck, pin v4.33.0, oleans Mathlib chauds. Le lake se choisit dans le kernelspec, pas dans le notebook.

Contrainte du REPL mesurée sur les précédents natifs : les import ne commitent l’environnement que seuls dans leur cellule — mélangés à d’autres commandes, ils sont ignorés silencieusement. D’où la cellule suivante.

import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
import Mathlib.Tactic

import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

import Mathlib.Tactic

--% env 0

Raw input

{"cmd": "import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv\nimport Mathlib.Tactic\n"}

Raw output

{"env": 0}

1. Un théorème Erdős prouvé, importé : Erdős–Ginzburg–Ziv

Énoncé (1935) : toute suite d’au moins 2n − 1 entiers contient une sous-suite de n éléments dont la somme est divisible par n. C’est un pilier de la combinatoire additive — le terrain où Erdős a le plus semé.

Mathlib embarque ce théorème (Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.lean) en quatre variantes : Int (divisibilité), ZMod (somme nulle), et leurs déclinaisons Multiset. La preuve procède par induction sur la décomposition en facteurs premiers de n, le cas premier étant délégué en amont dans le même fichier.

#check @Int.erdos_ginzburg_ziv
#check @ZMod.erdos_ginzburg_ziv

#check @Int.erdos_ginzburg_ziv @Int.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ℤ),
  2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i

#check @ZMod.erdos_ginzburg_ziv @ZMod.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n),
  2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0

--% env 1

Raw input

{"cmd": "#check @Int.erdos_ginzburg_ziv\n#check @ZMod.erdos_ginzburg_ziv\n", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "@Int.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ℤ),\n  2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "@ZMod.erdos_ginzburg_ziv : ∀ {ι : Type u_1} {n : ℕ} {s : Finset ι} (a : ι → ZMod n),\n  2 * n - 1 ≤ s.card → ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0"}],
 "env": 1}

Lecture des signatures. Le ι est un type d’index arbitraire, s : Finset ι la suite, l’hypothèse 2 * n - 1 ≤ #s le cardinal minimal, la conclusion une existence : un sous-ensemble t de taille n à somme divisible par n (variante Int) ou nulle dans ZMod n.

Premier geste de digestion : demander au noyau ce sur quoi repose la preuve.

#print axioms Int.erdos_ginzburg_ziv

#print axioms Int.erdos_ginzburg_ziv 'Int.erdos_ginzburg_ziv' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 2

Raw input

{"cmd": "#print axioms Int.erdos_ginzburg_ziv\n", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'Int.erdos_ginzburg_ziv' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 2}

Lecture des axiomes. La sortie donne les trois axiomes standard de Mathlib : propext, Classical.choice, Quot.sound. Classical.choice dit que la preuve est non constructive — accepté et whitelisté par nom explicite dans la politique d’axiomes du dépôt, jamais par wildcard. Le point décisif : pas de sorryAx. Le certificat est complet — la preuve existe, le noyau l’a vérifiée, et ce qui reste ce sont des choix fondationnels assumés.

2. Le témoin : EGZ appliqué et exhibé

EGZ est un énoncé d’existence. La digestion l’incarne sur un cas calculable : n = 3, la suite (0, 1, 1, 2, 2) dans ZMod 3 — exactement 2·3 − 1 = 5 éléments.

Le témoin {0, 1, 2} est de cardinal 3 et de somme 0 + 1 + 2 = 3 ≡ 0 (mod 3) :

example : Multiset.sum ({0, 1, 2} : Multiset (ZMod 3)) = 0 := by
  decide

example : Multiset.sum ({0, 1, 2} : Multiset (ZMod 3)) = 0 := by

  decide

--% env 3

Raw input

{"cmd": "example : Multiset.sum ({0, 1, 2} : Multiset (ZMod 3)) = 0 := by\n decide\n", "env": 2}

Raw output

{"env": 3}

Et l’énoncé d’existence s’applique mécaniquement — Mathlib fournit le théorème, on fournit le cardinal :

example : ∃ t ≤ ({0, 1, 1, 2, 2} : Multiset (ZMod 3)),
    Multiset.card t = 3 ∧ Multiset.sum t = 0 :=
  ZMod.erdos_ginzburg_ziv_multiset _ (by decide)

example : ∃ t ≤ ({0, 1, 1, 2, 2} : Multiset (ZMod 3)),

    Multiset.card t = 3 ∧ Multiset.sum t = 0 :=

  ZMod.erdos_ginzburg_ziv_multiset _ (by decide)

--% env 4

Raw input

{"cmd": "example : \u2203 t \u2264 ({0, 1, 1, 2, 2} : Multiset (ZMod 3)),\n    Multiset.card t = 3 \u2227 Multiset.sum t = 0 :=\n  ZMod.erdos_ginzburg_ziv_multiset _ (by decide)\n", "env": 3}

Raw output

{"env": 4}

Ce que cette paire de cellules montre : l’existence certifiée (deuxième cellule) et le témoin concret vérifié (première cellule) sont deux choses distinctes. Nous n’avons pas rejoué la preuve d’EGZ — c’est l’import qui certifie ; la digestion relie l’énoncé importé au cas calculé.

3. Le pattern conjecture-as-sorry : l’équation d’Erdős–Moser

L’équation 1^k + 2^k + ... + m^k = (m+1)^k. Pour k = 1 elle admet la solution triviale 1 + 2 = 3 (et elle seule) ; pour k ≥ 2, personne ne sait — aucun contre-exemple, aucune preuve, d’énormes bornes computationnelles (répertoriée dans la base erdosproblems.com et chez Wikipedia).

Formalisée en Lean, une conjecture ouverte s’écrit exactement comme un théorème — au sorry près :

theorem erdos_moser_conjecture :
    ∀ k m : ℕ, 2 ≤ k → (∑ i ∈ Finset.range m, (i + 1) ^ k) ≠ (m + 1) ^ k := by
  sorry

theorem erdos_moser_conjecture :🟨 declaration uses `sorry`

    ∀ k m : ℕ, 2 ≤ k → (∑ i ∈ Finset.range m, (i + 1) ^ k) ≠ (m + 1) ^ k := by

  sorry

--% env 5

--% prove 0

Raw input

{"cmd": "theorem erdos_moser_conjecture :\n    \u2200 k m : \u2115, 2 \u2264 k \u2192 (\u2211 i \u2208 Finset.range m, (i + 1) ^ k) \u2260 (m + 1) ^ k := by\n  sorry\n", "env": 4}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 3, "column": 2},
   "goal":
   "⊢ ∀ (k m : ℕ), 2 ≤ k → ∑ i ∈ Finset.range m, (i + 1) ^ k ≠ (m + 1) ^ k",
   "endPos": {"line": 3, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 30},
   "data": "declaration uses `sorry`"}],
 "env": 5}

#print axioms erdos_moser_conjecture

#print axioms erdos_moser_conjecture 'erdos_moser_conjecture' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

--% env 6

Raw input

{"cmd": "#print axioms erdos_moser_conjecture\n", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'erdos_moser_conjecture' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]"}],
 "env": 6}

example : (∑ i ∈ Finset.range 2, (i + 1) ^ 1) = (2 + 1) ^ 1 := by
  decide

example : (∑ i ∈ Finset.range 2, (i + 1) ^ 1) = (2 + 1) ^ 1 := by

  decide

--% env 7

Raw input

{"cmd": "example : (\u2211 i \u2208 Finset.range 2, (i + 1) ^ 1) = (2 + 1) ^ 1 := by\n decide\n", "env": 6}

Raw output

{"env": 7}

Le discriminant, en une sortie : 'erdos_moser_conjecture' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound].

Deux énoncés de forme syntaxique identique (theorem ... := by ...), et le noyau les sépare par leurs axiomes : la conjecture porte le trio standard plus sorryAx — c’est ce supplément qui dit que la preuve manque. C’est toute la mécanique du projet formal-conjectures : la base d’Erdős devient une collection d’énoncés theorem ... := by sorry, où chaque sorry est un ticket ouvert. Le benchmark du papier DeepMind mesure exactement la capacité d’un agent à faire tomber un sorryAx — le certificateur n’étant pas l’agent mais le noyau.

La troisième cellule rappelle pourquoi l’hypothèse 2 ≤ k est nécessaire : sans elle l’énoncé serait faux, puisque 1 + 2 = 3 (vérifié par decide). Un énoncé de conjecture mal borné est un faux ticket : il serait réfutable sans être intéressant.

4. Provenance, attribution et carte des dépendances

Élément	Provenance	Niveau de garantie
Énoncé EGZ	Erdős–Ginzburg–Ziv 1935	théorème (maths)
Preuve EGZ	`Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.lean`, pin `v4.33.0`	`lake build` + noyau ; axiomes `[propext, Classical.choice, Quot.sound]`
Conjecture Erdős–Moser	base erdosproblems.com (Bloom) ; projet Google DeepMind Formal Conjectures (arXiv:2605.13171, Firsching et al. 2026)	énoncé seul, `sorryAx`
Raccord corpus	Lean-7b/Lean-8 (agents, claims Erdős ancrés en #15209) ; lake `discrepancy_lean` #12839 (Beck-Fiala restatée) ; Lean-12 (sensitivity, Huang 2019)	—

Attribution honnête : la formalisation de l’équation d’Erdős–Moser ci-dessus est une restatement pédagogique locale — le projet formal-conjectures maintient ses propres énoncés ; nous n’importons ni ne reproduisons leur travail. La preuve d’EGZ n’est pas de ce dépôt : Mathlib la porte, ce notebook la consomme et l’expose.

5. Friction et chemin de découverte

Le nom nu échoue : #check erdos_ginzburg_ziv rend unknown constant — les théorèmes vivent sous préfixe de namespace (Int., ZMod.). Première sonde du smoke, premier réflexe à enseigner.
L’agrégateur ne suffit pas : le lake avait l’agrégateur Mathlib chaud, mais le module ErdosGinzburgZiv devait être construit explicitement (lake build Mathlib.Combinatorics.Additive.ErdosGinzburgZiv) avant le run — un import de feuille exige l’olean de la feuille.
Le lake se choisit avant le notebook : kernelspec per-lake (--cd dans l’argv), pas de %cd fonctionnel.

6. Exercices

-- Exercice 1 : EGZ pour n = 2. La suite (1, 0, 1) de ZMod 2 compte 3 = 2*2 - 1
-- elements ; il existe donc un sous-multiensemble de cardinal 2 et de somme
-- nulle. L'exhiber.
-- Indice : dans ZMod 2, 1 + 1 = 0.
-- TODO etudiant : remplacer le corps ci-dessous
def temoinEGZ2 : Multiset (ZMod 2) :=
  ({0} : Multiset (ZMod 2))

-- Doivent valoir 2 puis 0
#eval Multiset.card temoinEGZ2
#eval Multiset.sum temoinEGZ2

-- Exercice 1 : EGZ pour n = 2. La suite (1, 0, 1) de ZMod 2 compte 3 = 2*2 - 1

-- elements ; il existe donc un sous-multiensemble de cardinal 2 et de somme

-- nulle. L'exhiber.

-- Indice : dans ZMod 2, 1 + 1 = 0.

-- TODO etudiant : remplacer le corps ci-dessous

def temoinEGZ2 : Multiset (ZMod 2) :=

  ({0} : Multiset (ZMod 2))

-- Doivent valoir 2 puis 0

#eval Multiset.card temoinEGZ2 1

#eval Multiset.sum temoinEGZ2 0

--% env 8

Raw input

{"cmd": "-- Exercice 1 : EGZ pour n = 2. La suite (1, 0, 1) de ZMod 2 compte 3 = 2*2 - 1\n-- elements ; il existe donc un sous-multiensemble de cardinal 2 et de somme\n-- nulle. L'exhiber.\n-- Indice : dans ZMod 2, 1 + 1 = 0.\n-- TODO etudiant : remplacer le corps ci-dessous\ndef temoinEGZ2 : Multiset (ZMod 2) :=\n  ({0} : Multiset (ZMod 2))\n\n-- Doivent valoir 2 puis 0\n#eval Multiset.card temoinEGZ2\n#eval Multiset.sum temoinEGZ2\n", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 5},
   "data": "1"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "0"}],
 "env": 8}

-- Exercice 2 : le cas k = 3, m = 2 d'Erdos-Moser. Le membre gauche vaut
-- 1^3 + 2^3 = 9, le droit (2+1)^3 = 27 : ils different.
-- TODO etudiant : completez la preuve (une tactique suffit).
-- Ce sorry est volontairement le meme ticket ouvert que la section 3 :
-- tant qu'il est la, #print axioms du dessus raconte la meme histoire.
example : (∑ i ∈ Finset.range 2, (i + 1) ^ 3) ≠ (2 + 1) ^ 3 := by
  sorry

-- Exercice 2 : le cas k = 3, m = 2 d'Erdos-Moser. Le membre gauche vaut

-- 1^3 + 2^3 = 9, le droit (2+1)^3 = 27 : ils different.

-- TODO etudiant : completez la preuve (une tactique suffit).

-- Ce sorry est volontairement le meme ticket ouvert que la section 3 :

-- tant qu'il est la, #print axioms du dessus raconte la meme histoire.

example : (∑ i ∈ Finset.range 2, (i + 1) ^ 3) ≠ (2 + 1) ^ 3 := by🟨 declaration uses `sorry`

  sorry

--% env 9

--% prove 1

Raw input

{"cmd": "-- Exercice 2 : le cas k = 3, m = 2 d'Erdos-Moser. Le membre gauche vaut\n-- 1^3 + 2^3 = 9, le droit (2+1)^3 = 27 : ils different.\n-- TODO etudiant : completez la preuve (une tactique suffit).\n-- Ce sorry est volontairement le meme ticket ouvert que la section 3 :\n-- tant qu'il est la, #print axioms du dessus raconte la meme histoire.\nexample : (\u2211 i \u2208 Finset.range 2, (i + 1) ^ 3) \u2260 (2 + 1) ^ 3 := by\n  sorry\n", "env": 8}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 7, "column": 2},
   "goal": "⊢ ∑ i ∈ Finset.range 2, (i + 1) ^ 3 ≠ (2 + 1) ^ 3",
   "endPos": {"line": 7, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 7},
   "data": "declaration uses `sorry`"}],
 "env": 9}

-- Exercice 3 : la version multiset du cote Int.
-- TODO etudiant : afficher les axiomes de Int.erdos_ginzburg_ziv_multiset
-- (une commande #print axioms suffit) et comparer avec la section 1 :
-- meme preuve, meme axiomes attendus.
#check @Int.erdos_ginzburg_ziv_multiset

-- Exercice 3 : la version multiset du cote Int.

-- TODO etudiant : afficher les axiomes de Int.erdos_ginzburg_ziv_multiset

-- (une commande #print axioms suffit) et comparer avec la section 1 :

-- meme preuve, meme axiomes attendus.

#check @Int.erdos_ginzburg_ziv_multiset @Int.erdos_ginzburg_ziv_multiset : ∀ {n : ℕ} (s : Multiset ℤ), 2 * n - 1 ≤ s.card → ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum

--% env 10

Raw input

{"cmd": "-- Exercice 3 : la version multiset du cote Int.\n-- TODO etudiant : afficher les axiomes de Int.erdos_ginzburg_ziv_multiset\n-- (une commande #print axioms suffit) et comparer avec la section 1 :\n-- meme preuve, meme axiomes attendus.\n#check @Int.erdos_ginzburg_ziv_multiset\n", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "@Int.erdos_ginzburg_ziv_multiset : ∀ {n : ℕ} (s : Multiset ℤ), 2 * n - 1 ≤ s.card → ∃ t ≤ s, t.card = n ∧ ↑n ∣ t.sum"}],
 "env": 10}

Conclusion — limites et transmission

Ce qui est prouvé, importé, ouvert. Prouvé et importé : EGZ, consommé sans rejeu de preuve. Ouvert : Erdős–Moser, restatée avec un sorry assumé. Aucune nouveauté mathématique dans ce notebook — sa valeur est le geste : rendre inspectable la frontière entre certificat et conjecture.

Raccord. Lean-7b génère des preuves, Lean-8 orchestre des agents : la base d’Erdős formalisée est le terrain où ces agents se mesurent — la boucle est bouclée. Lean-12 montre l’autre bout de l’histoire : une conjecture (sensitivity) devenue théorème, preuve de Huang 2019.

Transmission. Trois exercices exécutables, deux #print axioms à lire soi-même, et un critère à retenir : le noyau ne lit pas les intentions, il lit les axiomes.

Retour au sommet