Prove2Me

lean_workbook_plus_34709

Proved

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

Solve the equation (x+a3−a)((x+12(2a3+a))2+34a2+1)=0(x+a^3-a)\left (\left (x+\dfrac {1}{2}(2a^3+a) \right )^2 + \dfrac {3} {4}a^2 +1\right ) = 0 for xx in real numbers.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34709 (a x : ℝ) : (x + a ^ 3 - a) * ((x + (1 / 2) * (2 * a ^ 3 + a)) ^ 2 + (3 / 4) * a ^ 2 + 1) = 0 ↔ x = a - a ^ 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph