> 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
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
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
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:
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]
