lean_workbook_plus_23000

Proved

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

For $a=b$ and $c=-2a+3$ we got the following ineauality \n

\frac{3}{64}(4 a - 3)^2 (48 a^2 - 104 a + 57)\geq 0

, which is true for all reals. Equality occurs for $(a.b,c)=(\frac{3}{4}, \frac{3}{4}, \frac{3}{2})$ and it's permutations.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23000 :  ∀ a b c : ℝ, a = b ∧ c = -2 * a + 3 → (3 / 64) * (4 * a - 3) ^ 2 * (48 * a ^ 2 - 104 * a + 57) ≥ 0   :=  by sorry

Source