lean_workbook_plus_52558

Disproved

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

Prove that:\n

2\,{\frac {a}{21\,a+75\,b}}+2\,{\frac {b}{21\,b+75\,c}}+2\,{\frac {c}{21\,c+75\,a}}+1/7+1/10\,\sqrt {{\frac {ab+ac+bc}{{a}^{2}+{b}^{2}+{c}^{2}}}}\leq 5\,{\frac {\sqrt {{a}^{2}+3\,ab}}{21\,a+75\,b}}+5\,{\frac {\sqrt {{b}^{2}+3\,bc}}{21\,b+75\,c}}+5\,{\frac {\sqrt {3\,ac+{c}^{2}}}{21\,c+75\,a}}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52558 :  ∀ a b c : ℝ, 2 * a / (21 * a + 75 * b) + 2 * b / (21 * b + 75 * c) + 2 * c / (21 * c + 75 * a) + 1 / 7 + 1 / 10 * Real.sqrt ((a * b + a * c + b * c) / (a ^ 2 + b ^ 2 + c ^ 2)) ≤ 5 * Real.sqrt (a ^ 2 + 3 * a * b) / (21 * a + 75 * b) + 5 * Real.sqrt (b ^ 2 + 3 * b * c) / (21 * b + 75 * c) + 5 * Real.sqrt (3 * a * c + c ^ 2) / (21 * c + 75 * a)   :=  by sorry

Source

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

View graph