3 ms·
Implementing the real Sieve is quite a challenge in any language: https://www.cs.hmc.edu/~oneill/papers/Sieve-JFP.pdf https://www.cs.hmc.edu/~oneill/papers/Sie
by thechao 2y ago
Implementing the real Sieve is quite a challenge in any language:
https://www.cs.hmc.edu/~oneill/papers/Sieve-JFP.pdf https://www.cs.hmc.edu/~oneill/papers/Sieve-JFP.pdf
- ykonstant 2y agoQuite; motivated by that paper I implemented a decent sieve of Eratosthenes with the standard wheel factorization in Lean 4: https://github.com/ykonstant1/esiv https://github.com/ykonstant1/esiv