lean_workbook_plus_19557

Disproved

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

Let $a,b,c>0$ , $a,b,c\in (0,\frac{1}{2}]$ ,prove that:\n\n $a(1-a)+b(1-b)+c(1-c) \le2/3.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19557 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 ∧ a ∈ Set.Icc 0 (1 / 2) ∧ b ∈ Set.Icc 0 (1 / 2) ∧ c ∈ Set.Icc 0 (1 / 2) → a * (1 - a) + b * (1 - b) + c * (1 - c) ≤ 2 / 3   :=  by sorry

Source

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

View graph