lean_workbook_plus_69720
ProvedThe function that describes PigeonBoi420's behavior is described by the sequence . We then have the inequality . Simplifying, we get , so . Using the quadratic formula, our roots are We only care about the positive root, which evaluates to ~ Therefore, PigeonBoi420 will haul in a number of pigeons greater than 420 in 15 days. So the answer is D.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69720 (n : ℕ) (a : ℕ → ℕ) (h₀ : ∀ x, a (x + 1) = a x + 3 * x) (h₁ : a 1 = 69) (h₂ : 420 < a n) : 15 ≤ n := by sorry
Source