lean_workbook_plus_12308

Proved

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

Substituting between the two given equations, \n \n $x + (7-x^{2})^{2} = 11$ \n \n $x^{4} - 14x^{2} + x +38 =0$ \n \n We can see that $x=2$ is a solution and, dividing the quartic by $x-2$ , we find that the other three solutions for $x$ are the roots of the cubic equation \n \n $x^{3} + 2x^{2} -10x - 19 =0$ . \n \n I don't see any nice solutions to this cubic.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12308  (x : ℝ)
  (h₀ : x + (7 - x^2)^2 = 11)
  (h₁ : x^4 - 14 * x^2 + x + 38 = 0) :
  x = 2 ∨ x^3 + 2 * x^2 - 10 * x - 19 = 0   :=  by sorry

Source

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

View graph