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 ). On January 31, 2024 9:42:56 PM PST, Mario Carneiro <[email protected]> wrote: >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. -- 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/B11CA9DC-6E50-4B44-80E4-60EA7E20912B%40panix.com.
