Prove2Me

lean_workbook_plus_8500

Proved

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

Prove Schur's inequality: m(m−n)(m−p)+n(n−m)(n−p)+p(p−m)(p−n)≥0m(m-n)(m-p) + n(n-m)(n-p) + p(p-m)(p-n) \geq 0 for m,n,p>0m, n, p > 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8500 (m n p : ℝ) (hm : 0 < m) (hn : 0 < n) (hp : 0 < p) : m * (m - n) * (m - p) + n * (n - m) * (n - p) + p * (p - m) * (p - n) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph