Strong PNT (Math Inc)

The blueprint of Strong PNT (Math Inc), read at commit 2f5835c3 (2025-09-10): one article for each of its 615 nodes whose Lean declarations it names and marks formalized, or in Mathlib. Its other 6 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 project gives no license, so this chapter has each node's title, Lean names, marks and dependencies, and links to its text in the blueprint, but not the text.

• Complex Analysis
• Log Derivative
• Riemann Zeta Function
• Zero Free Region
• Strong PNT

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.