Denesting a radical into three square roots

Proved

WorkbookSource.base_45131

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that: $\sqrt{10+\sqrt{24}+\sqrt{40}+\sqrt{60}}=\sqrt{2}+\sqrt3+\sqrt5$

Source: InternLM Lean-Workbook, record lean_workbook_45131 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_45131 : √(10 + √24 + √40 + √60) = √2 + √3 + √5  :=  by sorry

Source