lean_workbook_plus_10753

Proved

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

prove that: \n\n $(d^2+b^2)(c^2+a^2)\geq \frac{4}{6561}(8a+c)(8b+d)(8c+a)(8d+b)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10753 (a b c d : ℝ) : (d ^ 2 + b ^ 2) * (c ^ 2 + a ^ 2) ≥ (4 / 6561) * (8 * a + c) * (8 * b + d) * (8 * c + a) * (8 * d + b)   :=  by sorry

Source

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

View graph