RakeSieve
Natural-number sieves for Lean 4: arithmetic sequences, rakes, and a
formally verified (if laughably inefficient) prime sieve based on
RakeMap. Formerly published as leansieve.
Library pieces
ASeq— single arithmetic sequence (k + d·n)Rake— collection of sequences sharing the same deltadRakeMap— mapping between a rake and subsets of ℕPrimeGen— interface for a prime-generating algorithmPrimeSieve— generic logic of Eratosthenes-style sievesRakeSieve— rake-based prime sieve (proven correct; not practical)
Paper-facing theorems (Results.lean)
| Theorem | Meaning |
|---|---|
results_three_mem_R_two | 3 ∈ R 2 (base rake after sieving 2) |
results_three_le_of_mem_R_two | Every member of R 2 is ≥ 3 |
results_exists_prime_gt_of_primeGen | Any PrimeGen yields primes past any n (infinitude) |
results_exists_prime_gt_of_simpleGen | Infinitude via SimpleGen |
results_exists_prime_gt_of_rakeSieve | Infinitude via RakeSieve as a PrimeGen |
How RakeSieve works (sketch)
Start from ge2 := { d:=1, ks=[2] } and repeatedly partition on the lowest
constant term (a prime), keeping residue classes that are not multiples of that prime.
Sequence count grows by a factor of P−1 at each new prime P — worse than exponential.
step: 0 1 2 3 4 5 6 7 8 9
size: 1 2 8 48 480 5760 92160 1658880 36495360 1021870080
For a practical Lean prime sieve see
esiv; for counting primes via Selberg,
see selbergSieve.
Building
Toolchain: leanprover/lean4:v4.35.0-rc1 (see lean-toolchain).
git clone https://github.com/tangentproofs/rakesieve.git
cd rakesieve
lake exe cache get
lake build