ErdosMoser.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 1 contain sorry, 0 declared as axioms

The Erdős–Moser equation

For positive integers $k$ and $m$, let

$$S_k(m)=1^k+2^k+\cdots+(m-1)^k.$$

The Erdős–Moser conjecture says that $S_k(m)=m^k$ has only the solution $(k,m)=(1,3)$.

References:

Imports (1)

FormalConjecturesUtil

def ErdosMoser.powerSum The power sum $S_k(m)=\sum_{i=1}^{m-1} i^k$ line 41 source
Source documentation
The power sum $S_k(m)=\sum_{i=1}^{m-1} i^k$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.Ico, OfNat.ofNat, HPow.hPow
8 instances, coercions and auxiliary constants left out.
```
def powerSum (k m : ℕ) : ℕ :=
…
```
theorem ErdosMoser.erdos_moser_conjecture The only positive solution of $S_k(m)=m^k$ is $(k,m)=(1,3)$ sorry line 46 source
Source documentation
The only positive solution of $S_k(m)=m^k$ is $(k,m)=(1,3)$.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, ErdosMoser.powerSum, HPow.hPow, And
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_moser_conjecture :
    ∀ k m : ℕ, 0 < k → 0 < m → powerSum k m = m ^ k → k = 1 ∧ m = 3 := by
…
```
Mentions: ErdosMoser.powerSum
theorem ErdosMoser.powerSum_one_three The pair $(1,3)$ is the trivial solution of the Erdős–Moser equation line 52 source
Source documentation
The pair $(1,3)$ is the trivial solution of the Erdős–Moser equation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, ErdosMoser.powerSum, OfNat.ofNat, HPow.hPow
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem powerSum_one_three : powerSum 1 3 = 3 ^ 1 := by
…
```
Mentions: ErdosMoser.powerSum
theorem ErdosMoser.powerSum_two_three For $k=2$ and $m=3$, the left side is $1^2+2^2=5$, not $3^2$ line 57 source
Source documentation
For $k=2$ and $m=3$, the left side is $1^2+2^2=5$, not $3^2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Nat, ErdosMoser.powerSum, OfNat.ofNat, Ne, HPow.hPow
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem powerSum_two_three : powerSum 2 3 = 5 ∧ powerSum 2 3 ≠ 3 ^ 2 := by
…
```
Mentions: ErdosMoser.powerSum
theorem ErdosMoser.powerSum_zero Zero is a solution for every positive exponent, so the conjecture must require $m>0$ line 62 source
Source documentation
Zero is a solution for every positive exponent, so the conjecture must require $m>0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, ErdosMoser.powerSum, HPow.hPow
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, Finset.sum_congr, Finset.Ico, EmptyCollection.emptyCollection, Finset, Finset.Ico_eq_empty_of_le, LE.le, Membership.mem, Eq.refl, Nat.zero_pow, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem powerSum_zero (k : ℕ) (hk : 0 < k) : powerSum k 0 = 0 ^ k := by
…
```
Mentions: ErdosMoser.powerSum