Back to Problems

erdos_939.variants.euler

Specification

Euler had conjectured that the sum of $k - 1$ many $k$-th powers is never a $k$-th power, but this is false for $k=5$, as Lander and Parkin [LaPa67] found $$27^5+84^5+110^5+133^5=144^5$$. [LaPa67] Lander, L. J. and Parkin, T. R., "A counterexample to Euler's sum of powers conjecture." Math. Comp. (1967), 101--103.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_939.variants.euler : ¬ (∀ k ≥ 4, ∀ S : Finset ℕ, S.card = k - 1 →
    ¬ (∃ q, ∑ s ∈ S, s ^ k = q ^k))
ID: ErdosProblems__939__erdos_939.variants.euler
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.