Back to Problems

isSumOfThreeCubesRat_any

Specification

Any rational number is a sum of three rational cubes. First proved by Ryley in 1825, which can be found in [Ri1930]. The below parametrization is brought from the MSE answer [MSE]. [Ri1930] Richmond, H. W. "On Rational Solutions of $x^3 + y^3 + z^3 = R$." Proceedings of the Edinburgh Mathematical Society 2.2 (1930): 92-100. [MSE] Kieren MacMillan, Proving that any rational number can be represented as the sum of the cubes of three rational numbers, https://math.stackexchange.com/q/4480969

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem isSumOfThreeCubesRat_any (r : ℚ) : IsSumOfThreeCubes r
ID: Wikipedia__SumOfThreeCubes__isSumOfThreeCubesRat_any
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.