An upper bound on seventy-two times the square root of five
ProvedWorkbookSource.base_55900lean-workbooksource-checked
Show that .
Source: InternLM Lean-Workbook, record lean_workbook_55900 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_55900 : (72 * Real.sqrt 5 : ℝ) < 161 := by sorry
Source