Prove2Me

lean_workbook_plus_46981

Proved

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

On the basis of the Viete relations, we have: −ba=pp−1+p+1p-\frac{b}{a}=\frac{p}{p-1}+\frac{p+1}{p}, so b=−a2p2−1p(p−1)b=-a\frac{2p^{2}-1}{p(p-1)}, and ca=p(p+1)p(p−1)=p+1p−1\frac{c}{a}=\frac{p(p+1)}{p(p-1)}=\frac{p+1}{p-1} so c=ap+1p−1c=a\frac{p+1}{p-1}, thus a+b+c=a(1−2p2−1p(p−1)+p+1p−1)=a1p(p−1)a+b+c=a(1-\frac{2p^{2}-1}{p(p-1)}+\frac{p+1}{p-1})=a\frac{1}{p(p-1)} (1). Analogous b2−4ac=a2(2p2−1p(p−1))2−4a2p+1p−1=a21p2(p−1)2b^{2}-4ac=a^{2}\left(\frac{2p^{2}-1}{p(p-1)}\right)^{2}-4a^{2}\frac{p+1}{p-1}=a^{2}\frac{1}{p^{2}(p-1)^{2}} (2)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46981  (a b c p : ℝ)
  (h₀ : 0 < p ∧ p ≠ 1)
  (h₁ : a ≠ 0)
  (h₂ : (p - 1) * (p + 1) = 1)
  (h₃ : b = -a * (2 * p^2 - 1) / (p * (p - 1)))
  (h₄ : c = a * (p + 1) / (p - 1)) :
  b^2 - 4 * a * c = a^2 / (p^2 * (p - 1)^2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph