Prove2Me

lean_workbook_plus_53634

Disproved

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

The following inequality is equivalent to \n\n 3R2−s4−8Rrs2+2r2s2+16R2r2+8Rr3+r42(s2−4Rr−r2)≥0 3R^2 - \frac {s^4 - 8Rrs^2 + 2r^2s^2 + 16R^2r^2 + 8Rr^3 + r^4}{2(s^2 - 4Rr - r^2)}\geq 0 \n\n ⟺−s4+(6R2+8Rr−2r2)s2−24R3r−22R2r2−r4−8Rr3≥0 \Longleftrightarrow - s^4 + (6R^2 + 8Rr - 2r^2)s^2 - 24R^3r - 22R^2r^2 - r^4 - 8Rr^3\geq 0 \n\n ⟺−s4+(4R2+20Rr−2r2)s2−r(4R+r)3+2R((R−6r)s2+r(4R+r)(2r+5R))≥0 \Longleftrightarrow - s^4 + (4R^2 + 20Rr - 2r^2)s^2 - r(4R + r)^3 + 2R((R - 6r)s^2 + r(4R + r)(2r + 5R))\geq 0 \n\n can prove −s4+(4R2+20Rr−2r2)s2−r(4R+r)3≥0 - s^4 + (4R^2 + 20Rr - 2r^2)s^2 - r(4R + r)^3\geq 0 \n\n and \n\n (R−6r)s2+r(4R+r)(2r+5R)≥−4rs2+r(4R+r)(2r+5R) (R - 6r)s^2 + r(4R + r)(2r + 5R)\geq - 4rs^2 + r(4R + r)(2r + 5R) \n\n =r(−4s2+(4R+r)(2r+5R))≥r(−4(4R2+4Rr+3r2)+(4R+r)(2r+5R)) = r( - 4s^2 + (4R + r)(2r + 5R))\geq r( - 4(4R^2 + 4Rr + 3r^2) + (4R + r)(2r + 5R)) \n\n =r(5r+4R)(R−2r)≥0 = r(5r + 4R)(R - 2r)\geq 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53634 :
  ∀ (R r s : ℝ), 3 * R^2 - (s^4 - 8 * R * r * s^2 + 2 * r^2 * s^2 + 16 * R^2 * r^2 + 8 * R * r^3 + r^4) / (2 * (s^2 - 4 * R * r - r^2)) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph