Classification of a functional equation involving complementary cubes

Proved

WorkbookCorrected.plus_24563

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

corrected-formalizationlean-workbooksource-checked

A function $f:\mathbb{R}\to\mathbb{R}$ satisfies

f(x)+2f(\sqrt[3]{1-x^3})=x^3\qquad(x\in\mathbb{R})

if and only if $f(x)=\frac23-x^3$ for every real $x$ .

Formalization Note: The real cube root is expressed by the relation y³=1−x³, which uniquely specifies it. Unlike the original formalization, this statement does not omit the cube root or assume a second equation; it proves both necessity and sufficiency of the stated solution.

Source: InternLM Lean-Workbook, record lean_workbook_plus_24563 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_24563 : ∀ (f : ℝ → ℝ),
    (∀ x y : ℝ, y^3 = 1-x^3 → f x + 2*f y = x^3) ↔
    (∀ x : ℝ, f x = 2/3-x^3) := by sorry

Source

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

View graph