lean_workbook_plus_12070

Disproved

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

prove that: $(ab^2+bc^2+cd^2+a^2d)(a^2b+b^2c+c^2d+d^2a)\geq (acd+abd+abc+bcd)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12070 : ∀ a b c d : ℝ, (a * b ^ 2 + b * c ^ 2 + c * d ^ 2 + a ^ 2 * d) * (a ^ 2 * b + b ^ 2 * c + c ^ 2 * d + d ^ 2 * a) ≥ (a * c * d + a * b * d + b * c * a + b * d * c) ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph