lean_workbook_plus_4460

Disproved

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

Equality is held when $a = 1,b = \frac{{7 + 3\sqrt 5 }}{2},c = \frac{{3 + \sqrt 5 }}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4460 (a b c : ℝ) (ha : a = 1) (hb : b = (7 + 3 * Real.sqrt 5) / 2) (hc : c = (3 + Real.sqrt 5) / 2) : a * b * c = b + c - a   :=  by sorry

Source

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

View graph