lean_workbook_plus_75156Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)(a.1b+b.1c+c.1a+a.1a4)2≥((2a+b+c)(2a+1b+1c)16)2\left(\frac{a.\frac{1}{b} +b.\frac{1}{c}+c.\frac{1}{a}+a.\frac{1}{a}}{4}\right)^2 \ge \left(\frac{(2a+b+c)(\frac{2}{a}+\frac{1}{b}+\frac{1}{c})}{16}\right)^2(4a.b1+b.c1+c.a1+a.a1)2≥(16(2a+b+c)(a2+b1+c1))2Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_75156 : ∀ a b c : ℝ, (a * (1 / b) + b * (1 / c) + c * (1 / a) + a * (1 / a)) / 4 ≥ (2 * a + b + c) * (2 / a + 1 / b + 1 / c) / 16 := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph