Prove2Me

lean_workbook_plus_14728

Proved

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

Find the maximum value of F=(x1−a)(x2−a)+(x2−a)(x3−a)+(x3−a)(x4−a)+(x4−a)(x1−a)F = (x_1-a)(x_2-a) + (x_2-a)(x_3-a) + (x_3-a)(x_4-a) + (x_4-a)(x_1-a) given a=x1+x2+x3+x44a = \frac{x_1+x_2+x_3+x_4}{4} and x1,x2,x3,x4x_1, x_2, x_3, x_4 are real numbers.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14728 (x1 x2 x3 x4 a : ℝ) (h1 : a = (x1 + x2 + x3 + x4) / 4) : (x1 - a) * (x2 - a) + (x2 - a) * (x3 - a) + (x3 - a) * (x4 - a) + (x4 - a) * (x1 - a) ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph