lean_workbook_plus_73697

Disproved

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

$9 < 4st$ and $9(s - 1)(t - 1) < 4st$ and $9(s + t - 2) < 4st$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73697 (s t : ℝ) : 9 < 4 * s * t ∧ 9 * (s - 1) * (t - 1) < 4 * s * t ∧ 9 * (s + t - 2) < 4 * s * t   :=  by sorry

Source