Prove2Me

lean_workbook_plus_14207

Proved

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

Let p=xyzp=xyz . z×z\times first equation minus third is z(p−2)=−4z(p-2)=-4 x×x\times second equation minus first is x(p−3)=−1x(p-3)=-1 y×y\times third equation minus second is y(p−5)=−2y(p-5)=-2 Multiplying, we get p(p−2)(p−3(p−5)=−8p(p-2)(p-3(p-5)=-8 Which is p4−10p3+31p2−30p+8=0p^4-10p^3+31p^2-30p+8=0 Which is (p−1)(p−4)(p2−5p+2)=0(p-1)(p-4)(p^2-5p+2)=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14207  (x y z p : ℝ)
  (h₀ : p = x * y * z)
  (h₁ : x * (p - 3) = -1)
  (h₂ : y * (p - 5) = -2)
  (h₃ : z * (p - 2) = -4) :
  p^4 - 10 * p^3 + 31 * p^2 - 30 * p + 8 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph