Formal target: Corpus.WikipediaErdosMoser.erdos_moser_conjecture

The only positive solution of $S_k(m)=m^k$ is $(k,m)=(1,3)$.

Exact formal statement

∀ (k m : Nat),
  LT.lt.{0} 0 k →
    LT.lt.{0} 0 m →
      Eq.{1} (Corpus.WikipediaErdosMoser.powerSum k m) (HPow.hPow.{0, 0, 0} m k) → And (Eq.{1} k 1) (Eq.{1} m 3)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record