A cyclic quartic comparison under a quartic relation

Proved

WorkbookCorrected.base_34589

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

corrected-formalizationlean-workbooksource-checked

Let $a,b,c,d \geq 0$ such that $2(a^4+b^4+c^4+d^4) = a^2b^2+b^2c^2+c^2d^2+d^2a^2+2$ . Prove that $ab^3+bc^3+cd^3+da^3+1 \geq a^3b+b^3c+c^3d+d^3a$ .

Source: InternLM Lean-Workbook, record lean_workbook_34589 (Apache-2.0). Natural-language proposition preserved; missing source domain assumptions restored. Proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookCorrected.base_34589 (a b c d : ℝ) (source_domain_a : 0 ≤ a) (source_domain_b : 0 ≤ b) (source_domain_c : 0 ≤ c) (source_domain_d : 0 ≤ d) (h : 2 * (a ^ 4 + b ^ 4 + c ^ 4 + d ^ 4) = a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * d ^ 2 + d ^ 2 * a ^ 2 + 2) : a * b ^ 3 + b * c ^ 3 + c * d ^ 3 + d * a ^ 3 + 1 ≥ a ^ 3 * b + b ^ 3 * c + c ^ 3 * d + d ^ 3 * a  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_34589; Apache-2.0

View graph