lean_workbook_plus_18665

Disproved

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

Let be $a,b,c\in \mathbb{R}$ such that $ab + bc + ca + abc = a^2 + b^2 + c^2$ . Prove that $a,b,c$ can't all be nonpositives .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18665 : ∀ a b c : ℝ, a * b + b * c + c * a + a * b * c = a ^ 2 + b ^ 2 + c ^ 2 → ¬(a ≤ 0 ∧ b ≤ 0 ∧ c ≤ 0)   :=  by sorry

Source