Prove2Me

lean_workbook_plus_71624

Proved

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

It is equivalent to\n y+13=−(x+1)(x−1)2,\frac{y+1}{3}=-(x+1)(x-1)^2,\n z+14=−(y+1)(y−1)2,\frac{z+1}{4}=-(y+1)(y-1)^2,\n x+15=−(z+1)(z−1)2.\frac{x+1}{5}=-(z+1)(z-1)^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71624 : ∃ x y z : ℝ, (y + 1) / 3 = -(x + 1) * (x - 1) ^ 2 ∧ (z + 1) / 4 = -(y + 1) * (y - 1) ^ 2 ∧ (x + 1) / 5 = -(z + 1) * (z - 1) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph