Prove2Me

lean_workbook_plus_35437

Proved

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

Let a,b,ca,b,c be reals such that a2+b2+c2+abc=4.a^2+b^2+c^2+abc=4 . Prove that\n\n

a2+kb+kc+abc≤4+k22a^2+kb+kc+ abc \leq 4+ \frac{k^2}{2}

Where k>0.k>0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35437 (a b c k : ℝ) (ha : a^2 + b^2 + c^2 + a * b * c = 4) (hb : 0 < k) : a^2 + k * b + k * c + a * b * c ≤ 4 + k^2 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph