Twin prime conjecture

Identifier: F:twin-prime-unbounded
Proof route: Not assigned
External status: open
Axiom footprint: Empty

Recorded description

For every natural number n there is a prime p with n < p such that p + 2 is also prime; equivalently, there are infinitely many twin primes.

Formal statement

theorem TwinPrime.unbounded : ((n : AxNat) -> Exists.{1} AxNat (fun (p : AxNat) => And (AxNat.lt n p) (And (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) p) ((d : AxNat) -> ((hd : AxNat.dvd d p) -> Or (Eq.{1} AxNat d (AxNat.succ AxNat.zero)) (Eq.{1} AxNat d p)))) (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) (AxNat.add p (AxNat.succ (AxNat.succ AxNat.zero)))) ((d : AxNat) -> ((hd : AxNat.dvd d (AxNat.add p (AxNat.succ (AxNat.succ AxNat.zero)))) -> Or (Eq.{1} AxNat d (AxNat.succ AxNat.zero)) (Eq.{1} AxNat d (AxNat.add p (AxNat.succ (AxNat.succ AxNat.zero))))))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-08-14",
  "established_by": "not established in this ledger",
  "source": "proposition extracted from the S:number strand of the math-education concept graph; statement authored here, nothing copied",
  "prior_art": [
    {
      "citation": "Zhang 2014; Maynard and Tao 2014",
      "establishes": "bounded gaps -- some gap of size at most 246 recurs infinitely often -- which does NOT settle the gap-2 case"
    }
  ]
}