The Erdos-Moser Local Prime Obstruction

Abstract

Moser’s local prime obstruction makes the predecessor of every Erdos-Moser solution squarefree.

Theorem 1.1 (Every prime divisor of the predecessor satisfies Moser’s obstruction).

$$\begin{array}{r}\forall m,k\in \mathbb{N},\\ 1<m\wedge 0<k\wedge \sum _{i\in \mathrm{range}\left(m\right)}{i}^k=m^k\Rightarrow \\ (\forall p\in \mathbb{N},\mathrm{Prime}\left(p\right)\Rightarrow p\mid (m-1)\Rightarrow ((p-1)\mid k\wedge p\mid (\lfloor (m-1)/p\rfloor +1)\wedge \neg p^2\mid (m-1)))\wedge \mathrm{Squarefree}\left(m-1\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/PrimeForms/Obstructions/ErdosMoserLocalObstruction.erdos_moser_local_obstruction (✓ std3). ∎

Citation. Pieter Moree (2013). Moser’s mathemagical work on the equation 1^k + 2^k + … + (m−1)^k = m^k. DOI: 10.1216/rmj-2013-43-5-1707.

Commentary.

Moser (1953); literature attestation via Moree (2013), Theorem 2, which records Moser’s proof.

For each prime p dividing m - 1, write q for the natural-number quotient (m - 1) / p. The displayed floor notation denotes this integer quotient, never rational division.

The proof partitions the power sum into q complete residue blocks in ZMod p, explicitly transports the Finset.range p natural indices to ZMod p and then to its unit group, and applies the finite-field power-sum dichotomy. The zero branch is impossible, while the minus-one branch gives p dividing q + 1.

If p squared also divided m - 1, exact natural division would make p divide q, contradicting p dividing q + 1. The resulting exclusion for every prime is precisely squarefreeness. No parity assumption on k is used, and no claim is made that the open Erdos-Moser equation has no further solutions.

References

• Truth anchor: D5/S3/PrimeForms/Obstructions/ErdosMoserLocalObstruction.erdos_moser_local_obstruction