lean_workbook_plus_8309

Proved

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

The volume of the $V-GFN '$ pyramid is

V_{V-GFN'}= \frac{1}{3} \cdot \frac{GF \cdot FN'}{2} \cdot \sin 60^{\circ} \cdot VF = \frac{1}{3} \cdot \frac{\frac{9k}{2} \cdot 3k}{2}\cdot \frac{\sqrt{3}}{2} \cdot 9k = \frac{81 \sqrt{3}}{8} k^3

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8309 (k : ℝ) : (1 / 3 * (9 * k / 2 * 3 * k / 2) * Real.sqrt 3 / 2 * 9 * k) = 81 * Real.sqrt 3 / 8 * k ^ 3   :=  by sorry

Source