The Erdős–Moser equation: 1^k + 2^k + … + (m−1)^k = m^k has only the solution k = 1, m = 3
Difficulty 65: elementary to state, with no method for excluding solutions beyond astronomical bounds from Bernoulli-number congruences and continued fractions; below Agoh–Giuga (69.5) and Lehmer (72) because it has a smaller literature and fewer failed structural attacks, close to union-closed sets (66). Application value 1.5 and leverage 6: self-contained; the lowest in the number-theory set.
The problem
Does 1^k + 2^k + … + (m−1)^k = m^k have any solution other than k = 1, m = 3?
- 1One solution known: k=1, m=3
- 2Algebra pins k/m near ln 2
- 3Continued fractions prune candidates
- 4Any other has billions of digits
Statement. For positive integers and , compare the sum of the first -th powers with the next -th power: The asks when they are equal. The only known solution is : . In Lean the corpus defines as this sum and states that forces .
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Harmonic analysisTheory
- Step 3
- Then
- The Erdős–Moser equation: 1^k + 2^k + … + (m−1)^k = m^k has only the solution k = 1, m = 3The problem
State of the art
Moser (1953) showed that any further solution has (see Moree's survey). Butske, Jaje and Mayernik (2000) replaced estimates by exact computation and raised the bound to . Gallot, Moree and Zudilin (2011) used continued fractions of (the quantity must be a convergent) to reach . Moree also gives congruence conditions on (for example ). All of this narrows where a solution could hide but gives no route to excluding one.
Realistic applications
None. The problem is a probe of how power sums and Bernoulli polynomials interact; the tools (Bernoulli number congruences, continued fractions with huge denominators) are classical number-theory machinery.
What counts as solved
A Lean proof of erdos_moser_conjecture as stated, or an explicit counterexample with large enough that the kernel can still check the identity by computation (probably with a certified bignum procedure).
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
Statement: ErdosMoser.erdos_moser_conjecture in formal-conjectures, with the small helper powerSum shown in the statement; only core Lean and Mathlib (Finset.Ico, Finset.sum) are used, so no new definitions are needed. The file also proves sanity checks (powerSum 1 3 = 3^1 by decide) that a reviewer should keep. A counterexample would be an explicit pair whose identity Lean can check with kernel arithmetic on very large integers; a proof must handle all . Use Comparator to pin the statement.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
Bounds come from computation with Bernoulli numbers and continued fractions; excluding all solutions needs a new argument.
Bottlenecks
ranked by votes- #1TheoryNo exclusion argument
Congruence and continued-fraction constraints leave a sparse set of candidates but never reduce to a contradiction.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.
Progress
- Jan 1, 2011Continued-fraction method to 10^1,667,658,416source
Gallot, Moree and Zudilin (Math. Comp. 80; year only known).
- Jan 1, 2000Exact computation to 10^9,321,155source
Butske, Jaje and Mayernik (Math. Comp. 69; year only known).
- Jan 1, 1953Moser's boundsource
Leo Moser shows any other solution is astronomically large (Scripta Mathematica 19).