There is no largest prime

Identifier: F:nat-exists-prime-gt
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural number n there is a prime p with n < p. Equivalently, there are infinitely many primes.

Formal statement

theorem Nat.exists_prime_gt : ((n : AxNat) -> Exists.{1} AxNat (fun (p : AxNat) => And (AxNat.lt n p) (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))))))

Dependencies

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

11 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.exists_prime_gt

Kind: kernel-term
Status: checked

Supports: For every natural number n there is a prime p with n < p.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- exists_prime_gt 2>/dev/null | grep -xFc 'Nat.exists_prime_gt	3	((x0 : AxNat) -> Exists.{1} AxNat (fun (x1 : AxNat) => And (AxNat.lt x0 x1) (And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x1) (((x2 : AxNat) -> ((x3 : AxNat.dvd x2 x1) -> Or (Eq.{1} AxNat x2 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x2 x1)))))))')" -ge 1

Evidence notes

`build_nat_prelude` admits this through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type. Euclid's argument, done over N with no subtraction: take m = n! + 1, which is >= 2 because 1 <= n! (`one_le_factorial`), and let q be a prime dividing it (`exists_prime_dvd`). If q <= n then `dvd_factorial_of_le` gives q | n!, and with q | n!+1 `dvd_add_right_cancel_of_pos` yields q | 1, refuted by `not_dvd_one_of_two_le`. So n <= q, and the n = q case falls to the same contradiction after transporting n <= n along the equality, leaving n < q. The command matches the FULL RENDERED TYPE (grep -qxF), not the theorem name: lane `nat-prime-divisor` measured that a name-only checker survives a weakened statement -- spelling a primality bound `1 <= p` instead of `2 <= p` still type-checks, still admits, and is satisfied by p = 1. The kernel cannot see a weaker statement; only the type can.

footprint-Nat.exists_prime_gt

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`theorem_axiom_footprint` reports `nat Nat.exists_prime_gt 0` and `integer Nat.exists_prime_gt 0`. `nat_axiom_inventory` bounds it by enumerating the whole trusted surface: a theorem cannot depend on a trusted declaration the environment does not contain. Counting `Declaration::Axiom` alone would not suffice -- `Opaque` has no proof body and `Quotient` admits `Quot.sound` -- so all three kinds are covered.

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": [
    {
      "who": "Euclid",
      "what": "Elements, Book IX, Proposition 20",
      "year": -300,
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}