lean_workbook_plus_66459

Proved

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

And so $\boxed{f(x)=\frac{x^3+8x}6+\frac{-(x-2\left\lfloor\frac x2\right\rfloor)^3+6(x-2\left\lfloor\frac x2\right\rfloor)^2-8(x-2\left\lfloor\frac x2\right\rfloor)}6}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66459 (x : ℝ) : ∃ f : ℝ → ℝ, f x = (x^3 + 8*x)/6 + (-(x - 2*Int.floor (x/2))^3 + 6*(x - 2*Int.floor (x/2))^2 - 8*(x - 2*Int.floor (x/2)))/6   :=  by sorry

Source

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

View graph