lean_workbook_plus_27050

Disproved

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

Prove \n $\frac{1}{6a^2+1}+\frac{1}{6b^2+1}+\frac{1}{6c^2+1}\geq \frac{9}{5}$ when $a+b+c=1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27050 : ∀ a b c : ℝ, a + b + c = 1 → 1 / (6 * a ^ 2 + 1) + 1 / (6 * b ^ 2 + 1) + 1 / (6 * c ^ 2 + 1) ≥ 9 / 5   :=  by sorry

Source

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

View graph