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 <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.
