lean_workbook_plus_19276

Proved

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

For prime numbers $p$ and $q$ , $p+q = 102$ and $p>q.$ What is the least possible value of $p-q$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19276 {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p > q) (h : p + q = 102) : 16 ≤ p - q   :=  by sorry

Source