Prove2Me

lean_workbook_plus_31223

Disproved

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

Let b=a+kb=a+k , c=b+lc=b+l , d=c+md=c+m , e=d+ne=d+n , f=e+pf=e+p . The inequality becomes ((k+l)2+(m+n)2+(k+l+m+n)2+(l+m)2+(n+p)2+(l+m+n+p)2)2>2(k+m+p)2.(\sqrt{(k+l)^2+(m+n)^2+(k+l+m+n)^2}+\sqrt{(l+m)^2+(n+p)^2+(l+m+n+p)^2})^2>2(k+m+p)^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31223 : ∀ k l m n p : ℝ, (Real.sqrt ((k + l) ^ 2 + (m + n) ^ 2 + (k + l + m + n) ^ 2) + Real.sqrt ((l + m) ^ 2 + (n + p) ^ 2 + (l + m + n + p) ^ 2)) ^ 2 > 2 * (k + m + p) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph