PrimeNumberTheoremAnd

The objective of this project is to formalize in Lean the Prime Number Theorem (with classical error term), as well as related results such as the Prime Number Theorem in Arithmetic Progressions. A stretch goal would be to obtain the Chebotarev density theorem. We are also hosting the Integrated Explicit Analytic Number Theory network. A personal log describing the latter project may be found here.

Here is the blueprint for the project.

Zulip

The project is coordinated via a Lean Zulip channel.

Contributing

Contributions are welcome! Please read our Contributing Guide for instructions on how to claim issues, submit PRs, and participate in the project.

Quick contributions via gitpod

If you want to quickly contribute to the project without installing your own copy of lean, you can do so using gitpod. Simply visit: https://gitpod.io/new/#https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/, or click the button below:

All the required dependencies will be loaded (this takes a few minutes), after which you will be brought to a web-based vscode window, where you can edit the code, and submit PR's.

License

This project is licensed under the Apache 2.0 License. See the LICENSE file for details.