pith. machine review for the scientific record. sign in
def definition def or abbrev

attempt4

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 108noncomputable def attempt4 : ℝ := (phi + 1)^(2/phi)

proof body

Definition body.

 109
 110/-- Attempt 5: e ≈ φ^(φ + 1/φ)/φ = φ^(2φ-1)/φ
 111
 112    2φ - 1 ≈ 2.236
 113    φ^2.236 ≈ 2.963
 114    Divided by φ: 1.83 (too small) -/