lean_workbook_plus_28256

Proved

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

Solve for $x, y, z$ in the system\n $x^2+2+\frac{1}{x^2}=y^2$ \ny^2+2+\frac{1}{y^2}=z^2\n $z^2+2+\frac{1}{z^2}=x^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28256 (x y z : ℝ) (hx : x^2 + 2 + 1/x^2 = y^2) (hy : y^2 + 2 + 1/y^2 = z^2) (hz : z^2 + 2 + 1/z^2 = x^2) : x = y ∧ y = z ∧ z = x   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph