Least-prime search · complete increasing lists · witnessed powers · Constructive arithmetic

The first primes with explicit constructive bounds

k>0 ⇒ ∃ first k primes p₁<⋯<pₖ with pₖ<2^(2^k)

Construct the actual first k primes, prove that none is omitted, and bound the last prime by explicitly constructed powers of two.

Open the definition-aware map Read the final theorem See campaign milestone G022

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 810 native tactic lines and 75 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PE000C and follow only the lemmas and conservative definitions supporting first_primes_double_exponential_bound.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G021 milestone · G022 milestone → theorem and definition dependencies.
Major independently established statements: PE0001 foundation_primes_above_every_bound · PE0006 least_prime_above_exists_unique · PE0013 first_primes_list_exists · PE0010 prime_list_every_entry_is_prime · PE0012 prime_list_strictly_increasing · PE0011 prime_list_omits_no_smaller_prime · PE000C first_primes_double_exponential_bound.
Independently verified Alpha v34 checked-use theorem family: 19 dependency-curried kernel-checked theorem bodies · 75 proof prerequisites · 11 linked definitions · 14 definition-dependency arrows · 810 exact tactic lines · first admitted v28 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 862 bundle nodes; SHA-256 e56dda386bf60759d1bacda45417eacd7e6a67fd6e23799f002aac9964253ae1.
Exact mathematical boundary: Every successor is the globally least prime above its predecessor. This is not a sparse Bertrand chain. The bound theorem constructs the list and both power witnesses from k≠0 alone; the separate total-list theorem includes k=0.