lean_workbook_plus_59379

Proved

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

a,b,c>0 such that $a^2+b^2+c^2+abc=4$ , prove that $a+b+c \leq 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59379 (a b c : ℝ) (h : 0 < a ∧ 0 < b ∧ 0 < c) (habc : a * b * c = 1) (h : a^2 + b^2 + c^2 + a * b * c = 4) : a + b + c <= 3   :=  by sorry

Source

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

View graph