Zulip Chat Archive

I'm considering upstreaming the start of Consequences.lean to Mathlib, the parts which deal with the relations between the Chebyshev theta and psi functions (some of which I made some effort to tidy recently). I think those would be useful to have even without PNT, for example for prooving Chebyshev and Mertens type estimates.

Firstly are people happy for me to do this?

Secondly I was wondering what the correct thing to do concerning authorship is. Should the author listed in the Mathlib file be the name of the person who upstreamed, wwith a reference to the PNT project in the docstring, or should the original PNT contributors be listed? I assume the author has to be an actual person rather than just saying PrimeNumberTheoremAnd, it may not always be clear who actually contributed parts of our files without going back through the git history. Personally I have no strong views here but it would be useful to know what is compliant with Mathlib requirements whilst also recognising everyones contributions.

Ruben Van de Velde (Nov 29 2025 at 12:04):

Yes please! In general, I would attempt to check the git blame for who did the first major work for the copyright, yeah. I have some changes in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/423 to pass the flexible linter that was recently enabled in mathlib, so I'd suggest starting from there

Terence Tao (Nov 29 2025 at 14:59):

Thanks for taking the lead on this! I would defer to whatever is the accepted practice at Mathlib on this. Presumably as long as the upstreamed files contain some backreference to PNT+ then an interested party can in principle dive into the repository and work out finer-grained attributions to some extent.

Kim Morrison (Nov 30 2025 at 00:59):

Remember also the "authors:" line is doing double duty. As well as attempting to acknowledge contributions, it is also trying to provide a point of contact if there are questions about or problems with the file. (e.g. if a change in Lean breaks things, it is really helpful if "authors:" points to someone who I can ask for help, and be likely to get a response.)

Alastair Irving (Dec 14 2025 at 08:59):

Update: two of my PRs have made it into Mathlib v4.26.0: #32247 and #32252. Thank you to all those who left very helpful review comments. I see that @Ruben Van de Velde has PRs on PNT to bump to v4.26.0 and also to use the new Mathlib version of psi in Medium PNT. Once those are merged I'll also update Consequences.lean to use the new results. My upstreamed results also include the Chebyshev upper bound $\psi(x) \le cx$ so we could update Wiener.lean to avoid the dependence on the sieve.