lean_workbook_plus_24522

Disproved

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

We have : $2(p+q) \ge 4\sqrt{pq}$ and $p^2 \ge 3q$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24522 :  ∀ p q : ℝ, (2 * (p + q) ≥ 4 * Real.sqrt (p * q) ∧ p ^ 2 ≥ 3 * q)   :=  by sorry

Source