The eighth term of a pair of rational recurrences
ProvedWorkbookSource.problem_33900lean-workbooksource-checked
Define two sequences of rational numbers as follows: let and , and recursively define and . Find , leaving your answer in the exponential form .
Source: InternLM Lean-Workbook, record lean_workbook_33900 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_33900 (b : ℕ → ℚ) (a : ℕ → ℚ) (b0 : b 0 = 3) (a0 : a 0 = 2) (hb : ∀ n, b (n + 1) = (b n)^2 / a n) (ha : ∀ n, a (n + 1) = (a n)^2 / b n) : b 8 = (3^3281)/2^3280 := by sorry
Source