lean_workbook_plus_9183

Proved

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

If i) $f(1)=1$ ii) $f(2x)=4f(x)+6$ iii) $f(x+4)=4f(x)+4f(1)+8f(2)$ Find $f(6)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9183 (f : ℝ → ℝ) (hf1 : f 1 = 1) (hf2 : ∀ x, f (2 * x) = 4 * f x + 6) (hf3 : ∀ x, f (x + 4) = 4 * f x + 4 * f 1 + 8 * f 2) : f 6 = 106   :=  by sorry

Source

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

View graph