Prove2Me

lean_workbook_plus_402

Proved

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

p+q+r=1/a p+q+r=1/a \n\n pq+qr+pr=b/a pq+qr+pr=b/a \n\n →ab=(pq+qr+pr)(p+q+r)2 \rightarrow {ab}=\frac{(pq+qr+pr)}{{(p+q+r)}^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_402  (p q r a b : ℝ)
  (h₀ : p + q + r = 1 / a)
  (h₁ : p * q + q * r + r * p = b / a) :
  a * b = (p * q + q * r + r * p) / (p + q + r)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph