Almost all primes are partially regular

These files accompany the paper arXiv:xxxx.

The formal proofs provided in this work were developed and verified using Lean 4.28.0. 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

Theorem 1

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

Theorem 2 and Theorem 3

• task.md: natural language description of the problem
• .environment: specifies the Lean version
• source.tex
• theorem1.lean: this file is a verbatim copy of solution.lean in Biswal/theorem1/solution.lean.

Output files (Run with Lean 4.26.0)

Theorem 1

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

Theorem 2 and Theorem 3

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

License

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

Repository maintainers

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