Prove2Me

lean_workbook_plus_5654

Proved

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

  1. if f(1)=2006f(1)=2006 , then f(x)=1x+2005∀x>0\boxed{f(x)=\frac 1x+2005\quad\forall x>0} which indeed is a solution.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5654 (f : ℝ → ℝ) (hf: f = fun x => 1/x + 2005) : f 1 = 2006   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph