theorem
proved
term proof
pi_from_eight_quarters
show as:
view Lean formalization →
formal statement (Lean)
117theorem pi_from_eight_quarters :
118 8 * (π / 4) = 2 * π := by ring
proof body
Term-mode proof.
119
120/-! ## π and φ Relationship -/
121
122/-- π and φ are related through geometry:
123
124 1. **Golden angle**: 2π/φ² ≈ 137.5° (phyllotaxis)
125 2. **Pentagon**: Interior angle = 108° = 3π/5
126 3. **cos(π/5) = φ/2** (exact!)
127 4. **sin(π/10) = (φ-1)/2 = 1/(2φ)** (exact!)
128
129 These connect the circle (π) to the golden ratio (φ). -/