lean_workbook_plus_66172

Disproved

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

If $a \ge b \ge 1 \ge c$ , we can use $ab \le 2-c,(b^2-1)(1-c) \ge 0,(a-1)(1-c) \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66172 :  ∀ a b c : ℝ, a ≥ b ∧ b ≥ 1 ∧ 1 ≥ c → a * b ≤ 2 - c ∧ (b ^ 2 - 1) * (1 - c) ≥ 0 ∧ (a - 1) * (1 - c) ≥ 0   :=  by sorry

Source

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

View graph