This project has a blueprint, which is available at https://AlexKontorovich.github.io/PrimeNumberTheoremAnd/web/.
To use the tool, irst install local requirements using
python -pip install -r blueprint/requirements.txt
Then compile documentations using make doc
in the top-level directory. Alternatively, if the PDF is needed, type
cd blueprint
make pdf
For those using github's copilot (free for educators), it's very convenient to have the natural language statements
right next to the Lean to be formalized. So we write the blueprint TeX right in the *.lean document, separated by
delimiters /-%% text here %%-/
for multi-line and --%% text here
for single-line TeX. The code automatically
scrapes these and populates the blueprint accordingly.