Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Twin prime pair

Conjectura.Defs.Mathematics.NumberTheory.TwinPrimePair

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.Nat.Prime.Basic

/-! # Twin prime pair -/

namespace Conjectura.NumberTheory

/-- A **twin prime pair** is a pair of primes differing by two. -/
def IsTwinPrimePair (p q : ℕ) : Prop := p.Prime ∧ q.Prime ∧ q = p + 2

end Conjectura.NumberTheory