Prove2Me

lean_workbook_plus_3131

Proved

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

Let a≥b≥c≥0 a\ge b\ge c\ge 0 then a+b≥2a+b\ge 2 and \n\n

12a2+3+12b2+3≥4(a+b)2+6⇔\dfrac {1} {2a^2+3} +\dfrac {1} {2b^2+3} \ge \dfrac {4} {(a+b)^2+6} \Leftrightarrow (a−b)2⋅[(a+b)2+2ab−3]≥0(a-b)^2 \cdot [(a+b)^2+2ab-3]\ge 0

which is true since a+b≥2a+b\ge 2 so it is sufficies to prove \n\n

4(a+b)2+6+12c2+3≥35⇔\dfrac {4} {(a+b)^2+6} +\dfrac {1} {2c^2+3} \ge \dfrac {3} {5} \Leftrightarrow 4(3−c)2+6+12c2+3≥35⇔\dfrac {4} {(3-c)^2+6} +\dfrac {1} {2c^2+3} \ge \dfrac {3} {5} \Leftrightarrow 6c(4−c)(c−1)2≥06c(4-c)(c-1)^2 \ge 0

which is obvious since c≤1c\le 1

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3131  (a b c : ℝ)
  (h₀ : 0 ≤ a ∧ 0 ≤ b ∧ 0 ≤ c)
  (h₁ : a ≥ b ∧ b ≥ c)
  (h₂ : a + b ≥ 2) :
  1 / (2 * a^2 + 3) + 1 / (2 * b^2 + 3) ≥ 4 / ((a + b)^2 + 6) ↔ (a - b)^2 * ((a + b)^2 + 2 * a * b - 3) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph