TME-EMT

Stream: PrimeNumberTheorem+

[Harald Helfgott]

I want to flag something that seems potentially very useful for formalization efforts in explicit analytic number theory.

The TME-EMT now has an online wiki:
https://tme-emt-wiki-gitlab-io-9d3436.gitlab.io/index.html

It's nicely structured and gives a good sense of what is most important to the explicit analytic number theory community. Much of it seems well-suited as a top-level structure - blueprints could be a much higher-resolution level within this tree. I think it will be a very good, up-to-date complement to older, more linear sources - mainly Rosser-Schoenfeld - that have been guiding efforts recently.

(The wiki reflects the state of knowledge before some very recent work - as in, from the last couple of months. Of course the fact that it is a wiki makes it into a living document that is meant to be continually improved.)

[Terence Tao]

Looks like a valuable resource for future integration with PNT+. Inputting the results (without proofs) should be straightforward, especially with AI assistance: I just did this with Dusart's paper and it only took about an hour. The proofs may require more planning; I hope after formalizing the papers currently in process that we will get a better idea of how best to organize these.

[Harald Helfgott]

Thanks, Terry - that makes sense. I think this is a document that enables us to do some medium- to long-term planning, without being daunting, since it's all very modular and invites partial progress.

One thing that might also be worthwhile would be to enrich the tree in the TME-EMT wiki - with links to formalizations of statements and results, much as in the blueprint tree, but also with information on which statements depend on which others.. This will be particularly useful since many of these results will be improved over time (or have just been improved).

To humans in general: what do you suggest about encoding dependencies in a wiki? This sounds like something that must have been done, and done well, before.