lean_workbook_plus_10925

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find the value of $f(2007)$ if $f(n) = \begin{cases} 1 - f(n - 1) & \text{if } n \text{ is odd} \\ f(n - 1) & \text{if } n \text{ is even} \end{cases}$ and $f(0) = \frac{1}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10925 (f : ℕ → ℚ) (f0 : f 0 = 1 / 2) (f_rec : ∀ n, n > 0 → f n = if n % 2 = 0 then f (n - 1) else 1 - f (n - 1)) : f 2007 = 1 / 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph