lean_workbook_plus_79890

Disproved

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

Prove that $\frac{ab}{c^{2}}+\frac{ac}{b^{2}}+\frac{bc}{a^{2}}+\frac{a^{2}}{bc}+\frac{b^{2}}{ac}+\frac{c^{2}}{ab}-6\ge0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79890 : ∀ a b c : ℝ, (a * b / c ^ 2 + a * c / b ^ 2 + b * c / a ^ 2 + a ^ 2 / (b * c) + b ^ 2 / (a * c) + c ^ 2 / (a * b) - 6) ≥ 0   :=  by sorry

Source

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

View graph