Prove2Me

lean_workbook_plus_33770

Disproved

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

Prove that: \n\n (a−b)(a−c)(a−d)(b−c)(b−d)(c−d)≤27(a - b)(a - c)(a - d)(b - c)(b - d)(c - d) \le 27 \n\n P.S:Equality is held when \n\n a=4cos⁡210,b=4cos⁡250,c=4cos⁡270,d=0a = 4{\cos ^2}10,b = 4{\cos ^2}50,c = 4{\cos ^2}70,d = 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33770 : ∀ a b c d : ℝ, (a - b) * (a - c) * (a - d) * (b - c) * (b - d) * (c - d) ≤ 27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph