PDF slides from the talk where the project was launched: https://math.mit.edu/~drew/vantage/BuzzardSlides.pdf

What I really like is that this project will not blindly formalize the proof from the 90's. Instead they take a SOTA approach, streamlining and optimizing many parts of the proof. So it will result in a useful artifact for modern number theorists.

I wonder if after all that work, we might automatically reduce the proof and discover a simpler one that could have been included in the “margin”.

Very smart to open up the project from the start to make collaboration possible.

I have ambivalent feelings about this project. On one hand, I think this is great, it approaches things in the right way, and I think the project has a big chance of being very successful.

On the other hand, the more successful mathematics in Lean becomes, the more entrenched a type-theoretic outlook on formalised mathematics will become. I think that is highly problematic as it makes the expression of theorems and theories more involved and complicated than it needs to be. This is not a stopping block, and people like Buzzard can just power through this. Also, that's just my opinion. I am trying to go with Practal a different path and prove this opinion to be true, but that will take time.

I think this is awesome. I do wonder if projects like this will are the first step for humans to completely hand over proving to machines.

Why has Lean taken over the formalization world? Previously some big proofs were done in Coq, HOL, etc.

https://www.techrxiv.org/users/717330/articles/702287-on-fer...