lean_workbook_plus_2278

Proved

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

Prove that for any prime $p\ge5$ , there exists a prime $q$ such that $p<q<2p-2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2278 (p : ℕ) (hp : 5 ≤ p) (hp' : Nat.Prime p) : 
  ∃ q : ℕ, p < q ∧ q < 2 * p - 2   :=  by sorry

Source