Prove2Me

lean_workbook_plus_32380

Proved

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

For example, x=y=4,z=23x=y=4,z=\frac{2}{3} then (4−x2)(4−y2)(4−z2)=512(4-x^2)(4-y^2)(4-z^2)=512?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32380 {x y z : ℝ} (hx : x = 4) (hy : y = 4) (hz : z = 2 / 3) : (4 - x ^ 2) * (4 - y ^ 2) * (4 - z ^ 2) = 512   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph