Back to Problems

isSumOfThreeCubes_iff_mod_9

Specification

An integer `n : ℤ` can be written as a sum of three cubes (of integers) if and only if `n` is not `4` or `5` mod `9`.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem isSumOfThreeCubes_iff_mod_9 :
    answer(sorry) ↔ ∀ n : ℤ, IsSumOfThreeCubes n ↔ ¬(n ≡ 4 [ZMOD 9] ∨ n ≡ 5 [ZMOD 9])
ID: Wikipedia__SumOfThreeCubes__isSumOfThreeCubes_iff_mod_9
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.