Prove2Me

lean_workbook_plus_39014

Proved

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

Find all functions f:N→Nf:\mathbb{N} \rightarrow \mathbb{N} such that: f(1)=5f(1)=5 , f(f(n))=4n+9f(f(n))=4n+9 , f(2n)=2n+1+3f(2^n)=2^{n+1}+3 , ∀n∈N\forall n \in \mathbb{N}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39014 (f : ℕ → ℕ) (hf: f 1 = 5 ∧ ∀ n, f (f n) = 4*n + 9 ∧ f (2^n) = 2^(n+1) + 3) : ∃ f : ℕ → ℕ, f 1 = 5 ∧ ∀ n, f (f n) = 4*n + 9 ∧ f (2^n) = 2^(n+1) + 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph