lean_workbook_plus_79646

Disproved

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

And by C-S we have: $\frac{(2c-1)^2}{6a^2-4a+1}+\frac{(2b-1)^2}{6b^2-4b+1}\geq \frac{4c^2}{6(a^2+b^2)-4(a+b)+2}$ (because $a+b=1-c$ )

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79646 :
  ∀ a b c : ℝ,
    a + b + c = 1 ∧ a * b + b * c + c * a = c^2 →
    (2 * c - 1)^2 / (6 * a^2 - 4 * a + 1) + (2 * b - 1)^2 / (6 * b^2 - 4 * b + 1) ≥
    4 * c^2 / (6 * (a^2 + b^2) - 4 * (a + b) + 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph