A sum of cubes from a sum and product

Proved

WorkbookSource.problem_946

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

lean-workbooksource-checked

c+d=7, cd=9, what is $c^3+d^3$ ?

Source: InternLM Lean-Workbook, record lean_workbook_946 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved. The related Open record plus_27306 omits its variable declarations; this source explicitly declares real variables.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_946 (c d : ℝ) (h₁ : c + d = 7) (h₂ : c * d = 9) : c^3 + d^3 = 154  :=  by sorry

Source

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

View graph