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:
