Almost all primes are partially regular

These files accompany the paper arXiv:2602.05090.

The formal proofs provided in this work were developed and verified using Lean 4.34.0-rc2. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.

Input files

• problem.tex: natural language description of the problem
• .environment: specifies the Lean version

Output files (Run with Lean 4.34.0-rc2)

• PartialRegularity/problem.lean: translation of the problem statement into formal language (Lean)
• PartialRegularity/solution.lean: solution in formal language (Lean)

Additional files

Besides the end-to-end run above, we internally also conducted experiments where we provided AxiomProver with additional tools, such as AlexKontorovich/PrimeNumberTheoremAnd (although this dependency ended up not being needed). In one of these experiments, AxiomProver found that actually $C_{\alpha} = 10$ works for all $\alpha > 1/2$.

We provide the corresponding Lean files in extension/.

Verifying with Comparator

This repository can be verified against the formal problem statement with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:

lake env comparator comparator.json
lake env comparator comparator-extension.json

License

This repository uses the MIT License. See LICENSE for details.

Repository maintainers

• Evan Chen
• Kenny Lau
• Seewoo Lee
• Ken Ono
• Jujian Zhang