lean_workbook_plus_39652

Proved

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

Let $t=x+y$ , then the equation is equivalent to: \n $2(x+y)^3+3xy(10-x-y)=2000$ \n $\iff 2(t^2+10t+10^2)(t-10)=3xy(t-10)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39652 {x y t : ℝ} (h₁ : t = x + y) : (2 * (x + y) ^ 3 + 3 * x * y * (10 - x - y) = 2000) ↔ (2 * (t ^ 2 + 10 * t + 10 ^ 2) * (t - 10) = 3 * x * y * (t - 10))   :=  by sorry

Source

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

View graph