lean_workbook_plus_12206

Proved

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

Second one, part a, as Andreas said, it's equivalent to $(x+y)^{2}\geq 4xy$ , which is equivalent to $(x-y)^{2}\geq 0$ . And part b: with Cauchy (in Engel form) we get $\sum_{\text{cyc}}\frac{a}{b+2c+d}\geq \frac{(a+b+c+d)^{2}}{2ab+4ac+2ad+2bc+4bd+2cd}$ , so it's enough to prove that $(a+b+c+d)^{2}\geq 2ab+4ac+2ad+2bc+4bd+2cd$ , which is equivalent to $(a-c)^{2}+(b-d)^{2}\geq 0$ after expanding the LHS.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12206 :
  ∀ x y : ℝ, (x + y) ^ 2 ≥ 4 * x * y ∧
  ∀ a b c d : ℝ, (a + b + c + d) ^ 2 ≥ 2 * a * b + 4 * a * c + 2 * a * d + 2 * b * c + 4 * b * d + 2 * c * d   :=  by sorry

Source

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

View graph