lean_workbook_plus_67291

Proved

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

Let $a,b,c,d,e$ be real numbers so that : $a>0$ , $e<0$ , $b^2<\frac 83ac$ and $\frac a{2008}+\frac b{2007}+\frac c{2006}+\frac d{2005}+\frac e{2004}=0$ . Prove that : $a+b+c+d+e>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67291 (a b c d e : ℝ) (ha : 0 < a) (he : e < 0) (hb : b ^ 2 < 8 / 3 * a * c) (habcde : a / 2008 + b / 2007 + c / 2006 + d / 2005 + e / 2004 = 0) : a + b + c + d + e > 0   :=  by sorry

Source

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

View graph