PNT+

The blueprint of PNT+, read at commit 127b50e3 (2026-10-19): one article for each of its 383 nodes whose Lean declarations it names and marks formalized, or in Mathlib. Its other 20 nodes have no article, and a section of only those is left out: the map records what the project contains, not what it plans. A statement for which the blueprint marks no proof \leanok says so. Dependencies are the blueprint's \uses: a statement's under Depends on, a proof's under Proof depends on.

The text is the blueprint's, under its Apache-2.0 license: each page has a section's prose, remarks and examples in the blueprint's order, with each node's statement and proof where the node stands.

• The project
• Basic definitions and notation
• First approach: Wiener-Ikehara Tauberian theorem
• Second approach
• Third Approach
• Elementary Corollaries
• Explicit estimates
• Tertiary explicit estimates
• Iwaniec-Kowalski
• Bombieri-Vinogradov

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.