lean_workbook_plus_62795

Proved

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

Let $f$ be a function such that for all integers $x$ and $y$ applies $f(x+y) = f(x) + f(y) + 6xy + 1$ and $f(x) = f(-x)$ . Then $f(3)$ equals

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62795 (f : ℤ → ℤ) (hf1 : ∀ x y, f (x + y) = f x + f y + 6 * x * y + 1) (hf2 : ∀ x, f x = f (-x)) : f 3 = 26   :=  by sorry

Source