nx_proof_infinitude_primes.nx
buildroot/runtime/nx_proof_infinitude_primes.nx
about
nx_proof_infinitude_primes.nx -- Euclid's proof that there are
infinitely many primes (Wiedijk #11; Elements IX.20, ~300 BCE).
REAL nx_derive chain. HONEST disclaimer: structural verification
only -- see HONEST_QED_GAP_VS_HOL_LIGHT.md for the full gap.
Proof outline (Euclid's):
ASSUME for contradiction: there are only finitely many primes,
say p_1, p_2, ..., p_n.
[s1] Define N = p_1 * p_2 * ... * p_n + 1.
[s2] N > 1.
[s3] Every integer > 1 has a prime divisor (axiom: well-ordering)
[s4] N has a prime divisor q.
[s5] q is one of the p_i (since by assumption those are
all the primes).
[s6] q divides p_1 * p_2 * ... * p_n.
[s7] q divides N.
[s8] q divides (N - p_1*...*p_n) = 1.
[s9] CONTRADICTION (no prime divides 1).
THEREFORE the assumption is false: there are infinitely many primes ∎
dependencies 5 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_axioms.nxnx_derive.nx
imported by: nx_proof_infinitude_primes_test.nx
structs
| none |
consts
| 35 | const STMT_FINITE_PRIMES_ASSUMPTION: i64 = 100 |
| 36 | const STMT_DEFINE_N: i64 = 101 |
| 37 | const STMT_N_GT_1: i64 = 102 |
| 38 | const STMT_EVERY_INT_HAS_PRIME_DIV: i64 = 103 |
| 39 | const STMT_N_HAS_PRIME_DIV_Q: i64 = 104 |
| 40 | const STMT_Q_IS_ONE_OF_PI: i64 = 105 |
| 41 | const STMT_Q_DIVIDES_PRODUCT: i64 = 106 |
| 42 | const STMT_Q_DIVIDES_N: i64 = 107 |
| 43 | const STMT_Q_DIVIDES_1: i64 = 108 |
| 44 | const STMT_NO_PRIME_DIVIDES_1: i64 = 109 |
| 45 | const STMT_CONTRADICTION: i64 = 110 |
| 46 | const STMT_INFINITUDE_OF_PRIMES: i64 = 111 |
functions
| 48 | func nx_proof_infinitude_primes() -> i64 |