Rational Cube Sum

Let $n$ be a non-negative rational number such that there are rational $x$ and $y$ with $x^3 + y ^ 3 = n$. Show that there are non-negative rational $a$ and $b$ such that $a ^ 3 + b ^ 3 = n$.

_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.

import Mathlib.Data.Rat.Init

theorem solution (n : ℚ) (h1 : n ≥ 0) (h2 : ∃ x y, x ^ 3 + y ^ 3 = n) :
    ∃ a b : NNRat, a ^ 3 + b ^ 3 = n := sorry

Submit Solution

Login to submit a solution.

Recent Submissions