lean_workbook_plus_46257

Disproved

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

Check $a^2b + b^2c + c^2a \ge \frac{1}{3}(a + b + c) (ab + bc + ca)$ for $a = 3/4, b = 2, c = 1/4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46257 : (3 / 4 : ℝ) ^ 2 * 2 + 2 ^ 2 * (1 / 4) + (1 / 4) ^ 2 * (3 / 4) ≥ 1 / 3 * (3 / 4 + 2 + 1 / 4) * (3 / 4 * 2 + 2 * 1 / 4 + 1 / 4 * 3 / 4)   :=  by sorry

Source

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

View graph