lean_workbook_plus_35002

Proved

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

Let $f$ be a function taking real numbers such that for all reals $x\neq{0,1}$ , we have $f(x) + f(\frac{1}{1-x})=(2x-1)^2+f(1-\frac{1}{x})$ . What is $f(3)$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35002 (f : ℝ → ℝ) (hf : ∀ x, x ≠ 0 ∧ x ≠ 1 → f x + f ((1:ℝ) / (1 - x)) = (2 * x - 1) ^ 2 + f (1 - (1:ℝ) / x)) : f 3 = 113 / 9   :=  by sorry

Source

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

View graph