This is a temporary local fork of https://github.com/AlexKontorovich/PrimeNumberTheoremAnd by Alex Kontorovich et al. It only serves the following purposes:
- Bumped to a version needed for other repos.
- Upgraded to use the module system. (As a result, LeanCert and PrimeCert dependencies are cut out.)
- Sorries are removed, while making sure the PNT itself stays.
We will use Alex Kontorovich et al.'s main repo as soon as they fulfill the three criteria above.