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 <https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168109101> 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.
On Wed, Jan 31, 2024 at 3:55 AM 'Thierry Arnoux' via Metamath < [email protected]> wrote: > 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 > > > On 31/01/2024 07:04, Jim Kingdon wrote: > > 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 > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/8102B940-2AD8-4D32-9C26-42FD3ECDB73E%40panix.com > <https://groups.google.com/d/msgid/metamath/8102B940-2AD8-4D32-9C26-42FD3ECDB73E%40panix.com?utm_medium=email&utm_source=footer> > . > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/f5b7a37f-ea21-48d5-8d0b-cd90e2f18c0f%40gmx.net > <https://groups.google.com/d/msgid/metamath/f5b7a37f-ea21-48d5-8d0b-cd90e2f18c0f%40gmx.net?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvCCOJqDv5aCXetO36cqjAhc%2Be6UTDfMzWDJN23HkBnHA%40mail.gmail.com.
