Prove2Me

lean_workbook_plus_17116

Disproved

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

By Holder: \n (∑cyc1a2−ab+b2)2∑cyc(a2−ab+b2)≥27.\left(\sum_{cyc}\frac{1}{\sqrt{a^2-ab+b^2}}\right)^2\sum_{cyc}(a^2-ab+b^2)\geq27. \n Thus, it remains to prove that: \n 27≥9(a+b+c)a3+b3+c3⋅∑cyc(2a2−ab)27\geq\frac{9(a+b+c)}{a^3+b^3+c^3}\cdot\sum_{cyc}(2a^2-ab) , which is Schur.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17116 :
  ∀ a b c : ℝ, (1 / Real.sqrt (a ^ 2 - a * b + b ^ 2) + 1 / Real.sqrt (b ^ 2 - b * c + c ^ 2) + 1 / Real.sqrt (c ^ 2 - c * a + a ^ 2)) ^ 2 * (a ^ 2 - a * b + b ^ 2 + b ^ 2 - b * c + c ^ 2 + c ^ 2 - c * a + a ^ 2) ≥ 27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph