City Zhautykov 2023 Grade 8 Problem 3

Find all positive integer pairs $(x, y)$ such that $x ^ 3 = y ^ 2 + 1$.

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0.

import Mathlib.Data.Nat.Basic

def answer : Set (ℤ × ℤ) := sorry

theorem solution (x y : ℤ) (hx : 0 < x) (hy : 0 < y) : x ^ 3 = y ^ 2 + 1 ↔ (x, y) ∈ answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions