Prove2Me

lean_workbook_plus_10658

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Solve the system of equations x2−1=3u2x^2-1=3u^2 and x2+1=v2x^2+1=v^2 for integer solutions (x,u,v)(x, u, v).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10658 (x u v : ℤ) (h₁ : x^2 - 1 = 3 * u^2) (h₂ : x^2 + 1 = v^2) : ∃ x u v : ℤ, x^2 - 1 = 3 * u^2 ∧ x^2 + 1 = v^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph