Prime Number Theorem

[Jim Kingdon]

Looks like Terrence Tao is planning [1] to follow in the footsteps of Mario Carneiro [2] and formalize the Prime Number Theorem.

More seriously, it is really nice to see people getting excited about formalization. I figure this can only be a good thing.

[1] https://mathstodon.xyz/@tao/111847680248482955

[2] https://us.metamath.org/mpeuni/pnt.html

[Thierry Arnoux]

That's nice!

Lean really has a lot of traction, especially with such names as Terrence Tao, and with people like Andrej Bauer making publicity around it.

What I really like about it is that collaboration is fostered through tools such as the blue print and the dependency graph:

    https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html

This gives a good overview of the steps to reach the goal, and everyone can grab a piece (there is a Zulip Chat channel to synchronize about who does what).

And more importantly, this is a nice bridge between people who know the math but don't do formalization, and people who like to do formalization but are maybe not so sure about the advanced math involved.

I think it would be beneficial for the Metamath community to have such a tool, too. I've been thinking about it for a while.

BR,
_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8102B940-2AD8-4D32-9C26-42FD3ECDB73E%40panix.com.

[Mario Carneiro]

In the most technical sense, I wouldn't really call it "following in my footsteps", because the approach planned is not at all similar to the Erdos-Selberg method, and this is a good thing, I think mathlib has no need for the Erdos-Selberg proof (although I did port it to lean almost 5 years ago...). The complex analysis proof is much more productive in terms of its related results, and will be more useful for future projects like Fermat's Last Theorem (which has almost all areas of mathematics in its dependency tree). That's what the "and more" part of the project is about - PNT has been done before multiple times, it's old news, but *this way* of doing it will lead to other theorems that have not been formalized before. And the fact that big shot mathematicians are leading the charge makes me even more hopeful that (1) it will get done quickly and (2) it will actually prove theorems which are relevant and interesting to mathematicians.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f5b7a37f-ea21-48d5-8d0b-cd90e2f18c0f%40gmx.net.

[Jim Kingdon]

Thanks for clarifying the distinction between the Erdos–Selberg method and the complex analysis proof (you inspired me to go look at https://en.wikipedia.org/wiki/Prime_number_theorem which describes both proofs and some of the history). Interestingly enough that page does refer to a 2009 formalization of a complex analysis proof in HOL Light (I won't try to compare that to the current effort, as it could well have differences other than what proof system it is in).

Totally agree that a lot of what makes this exciting is getting big name mathematicians involved and collaborating (both with other mathematicians and with people who may be formalizers more than mathematicians, to the extent there is a difference).

As for Fermat's Last Theorem, I trust people are aware that Kevin Buzzard has a grant (starting in October) to lead an effort to formalize it (mentioned at https://www.imperial.ac.uk/people/k.buzzard ).

[savask]

> I think it would be beneficial for the Metamath community to have such a tool, too. I've been thinking about it for a while.

Thierry, I've been also thinking that Metamath could benefit from some collaboration, but I came to the conclusion that currently Metamath community is probably too small. It seems that there are lot more people involved in Lean, there are Lean-oriented courses at universities and there are people who do Lean nearly full-time (the closest we had to such a person was Mario, but it seems he has moved to other projects).

Needless to say, Lean has better tooling and PA tactics. I can't speak for others, but I personally don't attempt formalizing theorems myself anymore precisely because one has to spend a ridiculous amount of effort to formalize trivial things, like doing algebraic manipulations or proving tautologies.

That sounds too grim, but I like your "This gives a good overview of the steps to reach the goal, and everyone can grab a piece" idea :-) Maybe we could try to foster some collaboration by following Norm's suggestion or my one? Arguably, nearly all long-hanging fruit in the Metamath 100 list are done (besides, maybe some things related to geometry). People still look at that list, so it would be very useful in my opinion to break down the proof strategy into several steps and formalize the statement into Metamath (with empty proof). This can be placed in the set.mm github and tracked, for example, with an issue or a project, like Elementary Geometry and iset.mm do right now.