Prove2Me

A six-variable cyclic quadratic expression is nonnegative

Proved
WorkbookSource.base_41419

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked
  1. x,y,z,u,v,wx,y,z,u,v,w are real numbers,prove that:

(x−z)(v−z)+(y−x)(w−x)+(u−y)(z−y)+(w−v)(w+z)+(u−w)(x+u)+(v−u)(y+v)≥0(x-z)(v-z)+(y-x)(w-x)+(u-y)(z-y)+(w-v)(w+z)+(u-w)(x+u)+(v-u)(y+v)\geq 0

Source: InternLM Lean-Workbook, record lean_workbook_41419 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_41419 (x y z u v w : ℝ) : (x - z) * (v - z) + (y - x) * (w - x) + (u - y) * (z - y) + (w - v) * (w + z) + (u - w) * (x + u) + (v - u) * (y + v) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_41419; Apache-2.0

View graph