Prove2Me

lean_workbook_plus_75534

Proved

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

(1+a2)(1+a2+b2)(1+a2+b2+c2)≥16abc⇔(1+a2)(1+a2+b2)c2−16abc+(1+a2)(1+a2+b2)2≥0(1+a^2)(1+a^2+b^2)(1+a^2+b^2+c^2)\geq 16abc \Leftrightarrow (1+a^2)(1+a^2+b^2)c^2-16abc+(1+a^2)(1+a^2+b^2)^2\geq0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75534 (a b c : ℝ) : (1 + a ^ 2) * (1 + a ^ 2 + b ^ 2) * (1 + a ^ 2 + b ^ 2 + c ^ 2) ≥ 16 * a * b * c ↔ (1 + a ^ 2) * (1 + a ^ 2 + b ^ 2) * c ^ 2 - 16 * a * b * c + (1 + a ^ 2) * (1 + a ^ 2 + b ^ 2) ^ 2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph