Prove2Me

lean_workbook_plus_54302

Proved

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

Let xy=t\frac xy=t . The equation is t2−t+1t2+t+1=t\frac{t^2-t+1}{t^2+t+1}=t   ⟺  \iff t3+2t−1=0t^3+2t-1=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_54302 (x y t : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x = t * y) : (t^2 - t + 1) / (t^2 + t + 1) = t ↔ t^3 + 2 * t - 1 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph