Math-Inc Pulls

Stream: PrimeNumberTheorem+

[Steven Rossi]

Hi, I was just taking a shot at implementing DerivativeBound, and saw the blueprint says pulled from math-inc's strongpnt, do we still care about our own implementation of this?

[Alex Kontorovich]

If I recall, @Maksym Radziwill was working on DerivativeBound?

[Alex Kontorovich]

Actually, this reminds me: @Pietro Monticone, might this be a good time to move from "Outstanding Tasks" messages in zulip to a more proper "Issues" workflow? What do I need to do in github to implement that? Thanks!

[Pietro Monticone]

First of all, I apologise for the current lack of documentation, but it will be available in a month or so within the LeanProject template (adding MAINTAINING.md and MANAGING.md to the usual CONTRIBUTING.md).

I'll send you the instructions in DM since personal access tokens are required.

[Pietro Monticone]

Done.

[Maksym Radziwill]

Alex Kontorovich said:

If I recall, Maksym Radziwill was working on DerivativeBound?

Yes, it's available at https://github.com/maksym-radziwill/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/StrongPNT/DerivativeBound.lean I just never got around to PR-ing it to you... The bounds there are somewhat better than what was in the blueprint if I recall correctly.

Preston DMed that he has his own version ready, if you want to use his version instead no problem!

Also the proof of Borel-Caratheodory got simplified considerably but it's been stuck in review for close to three months in mathlib4 https://github.com/leanprover-community/mathlib4/pull/31719 .

[Ruben Van de Velde]

#31719 is not on the review queue because it hasn't been updated to the module system

[Steven Rossi]

Then are the next few theorems and definitions in the blueprint being worked on? I'm willing to take a shot if not

[Shreyas Srinivas]

Alex Kontorovich said:

Actually, this reminds me: Pietro Monticone, might this be a good time to move from "Outstanding Tasks" messages in zulip to a more proper "Issues" workflow? What do I need to do in github to implement that? Thanks!

It's not much. You need to set up a github project dashboard. Then you need to copy paste a bunch of scripts into a folder that manages the project dashboard for you.

[Kim Morrison]

(I still think "outstanding tasks" messages on Zulip are a much better solution than issues! :-)

[Steven Rossi]

Well just as an example with Maksym, not knocking on them but it is something that wasn't tracked in one of the outstanding task posts it was in a side discussion, so then the expectation would be update those more frequently or have people read every chat. I am biased for git though, am a swe full time

[Shreyas Srinivas]

Kim Morrison said:

(I still think "outstanding tasks" messages on Zulip are a much better solution than issues! :-)

The ETP would not have functioned nearly as well with Zulip based "Outstanding tasks". The project board approach is great from a maintainer's side. It's also an upgrade over issues + labels in that you get a good view of what's pending and what's done. The project dashboard was designed as an automated version of the outstanding tasks in Zulip in any case.

[Kim Morrison]

I understand, and disagree that issues are better. Zulip based "outstanding tasks" generates a much better social dynamic.

[Terence Tao]

Kim Morrison said:

I understand, and disagree that issues are better. Zulip based "outstanding tasks" generates a much better social dynamic.

In ETP we ended up having a hybrid format; issues were used to formally claim or disclaim tasks, but we still used the Zulip to informally announce the creation of issues and to discuss them. I think it worked well.

[Shreyas Srinivas]

The social dynamic issue is a fair point but it needs to be balanced with how tedious maintaining the "outstanding tasks" list can get. Not to mention the fact that if people are claiming and disclaiming things 24 hours a day across timezones, it puts a lot of strain on the maintainer to keep the message containing the task list up to date very frequently. In Zulip, I don't think users can authorise other users to edit messages on their behalf, so the burden falls on one person.

[Shreyas Srinivas]

With the ETP style approach, contributors are still encouraged to discuss and propose goals and discuss issues.

[Aayush Rajasekaran]

I'm just a hobbyist following this project (hoping to contribute at some point), but I would also favour a project dashboard that quickly shows you the status of issues. The Outstanding Tasks Zulip messages leave me dizzy :dizzy:

(same bias as @Steven Rossi above, though -- I'm also a full-time SWE)

[Alastair Irving]

A few comments on the blueprint for strong PNT:

• I don't think the current proof of LogOfAnalyticFunction works. Unless I'm missing something you can't just take logs here because the complex log is multivalued. The correct thing to do is to construct an antiderivative $g$ of $f'/f$ and then show that $\exp g = f$. Luckily Mathlib already has the result needed to construct the antiderivative, docs#DifferentiableOn.isExactOn_ball.
• I don't think lemma ZeroFactorization is needed. I think docs#meromorphicTrailingCoeffAt gives the value we want and we can use that in subsequent deffinitions without needing to appeal to a lemma.
• The various sums and products over zeros with multiplicity can be formalized using finsums over docs#MeromorphicOn.divisor.

I'm happy to help with some of this, time permitting, but as people have said above we do need some coordination of effort to avoid wasted work.