Prove2Me

lean_workbook_plus_26056

Proved

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

A function f f defined on the positive integers (and taking positive integers values) is given by: \n\n f(1)=1,f(3)=3\nf(2⋅n)=f(n)\nf(4⋅n+1)=2⋅f(2⋅n+1)−f(n)\nf(4⋅n+3)=3⋅f(2⋅n+1)−2⋅f(n), \begin{matrix} f(1) = 1, f(3) = 3 \nf(2 \cdot n) = f(n) \nf(4 \cdot n + 1) = 2 \cdot f(2 \cdot n + 1) - f(n) \nf(4 \cdot n + 3) = 3 \cdot f(2 \cdot n + 1) - 2 \cdot f(n), \end{matrix} \n\n for all positive integers n. n. Determine with proof the number of positive integers ≤1988 \leq 1988 for which f(n)=n. f(n) = n.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26056  (f : ℕ → ℕ)
  (h₀ : f 1 = 1)
  (h₁ : f 3 = 3)
  (h₂ : ∀ n, f (2 * n) = f n)
  (h₃ : ∀ n, f (4 * n + 1) = 2 * f (2 * n + 1) - f n)
  (h₄ : ∀ n, f (4 * n + 3) = 3 * f (2 * n + 1) - 2 * f n)
  : ∃ A : Finset ℕ, A.card = 1988 ∧ ∀ n ∈ A, f n = n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph