Two factorizations for a cubic function

Proved

WorkbookSource.problem_39005

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Write $f(x)={{6x^2-x^3}\over 8}={{x^2(6-x)}\over 8}$ then $f(x)-x={{x(x-2)(4-x)}\over 8}$ and $4-f(x)={{(4-x)^2(2+x)}\over 8}$ .

Source: InternLM Lean-Workbook, record lean_workbook_39005 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_39005 : ∀ x : ℝ, (6 * x ^ 2 - x ^ 3) / 8 - x = (x * (x - 2) * (4 - x)) / 8 ∧ 4 - (6 * x ^ 2 - x ^ 3) / 8 = ((4 - x) ^ 2 * (2 + x)) / 8  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_39005; Apache-2.0

View graph