lean_workbook_plus_42346

Disproved

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

$ab+bc+ca=(ab+bc-ca)+(bc+ca-ab)+(ab+ac-bc) \geq a^2+b^2+c^2,$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42346 : ∀ a b c : ℝ, a * b + b * c + c * a = (a * b + b * c - c * a) + (b * c + c * a - a * b) + (a * b + a * c - b * c) ∧ (a * b + b * c - c * a) + (b * c + c * a - a * b) + (a * b + a * c - b * c) ≥ a ^ 2 + b ^ 2 + c ^ 2   :=  by sorry

Source

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

View graph