def
definition
attempt2
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.Euler on GitHub at line 94.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
91 φ² = φ + 1 ≈ 2.618
92 1 - 1/φ = 1 - 0.618 = 0.382
93 Sum: 3.000 (too big) -/
94noncomputable def attempt2 : ℝ := phi^2 + (1 - 1/phi)
95
96/-- Attempt 3: e ≈ 2 + 1/φ²
97
98 1/φ² = φ - 1 = 0.618
99 Wait: 1/φ² = (φ-1)² = 0.382
100 2 + 0.382 = 2.382 (too small) -/
101noncomputable def attempt3 : ℝ := 2 + 1/phi^2
102
103/-- Attempt 4: e ≈ (φ + 1)^(2/φ)
104
105 φ + 1 = φ² ≈ 2.618
106 2/φ ≈ 1.236
107 2.618^1.236 ≈ 3.34 (too big) -/
108noncomputable def attempt4 : ℝ := (phi + 1)^(2/phi)
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) -/
115noncomputable def attempt5 : ℝ := phi^(phi + 1/phi) / phi
116
117/-! ## Continued Fraction Connection -/
118
119/-- e has a beautiful continued fraction:
120
121 e = 2 + 1/(1 + 1/(2 + 1/(1 + 1/(1 + 1/(4 + 1/(1 + 1/(1 + ...)))))))
122
123 Pattern: [2; 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8, ...]
124