Prove2Me

lean_workbook_plus_36284

Proved

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

Prove that 22+22+2+2=2−2+2\frac{\sqrt{2}}{\sqrt{2+\sqrt{2}}\sqrt{2+\sqrt{2+\sqrt{2}}}}=\sqrt{2-\sqrt{2+\sqrt{2}}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36284 : (√ 2) / (√ (2 + √ 2) * √ (2 + √ (2 + √ 2))) = √ (2 - √ (2 + √ 2))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph