Not peer reviewed, Lean proofs are 100,000 lines long and Lean has bugs:

https://cr.yp.to/proofs.html

Who is going to wade through this?

They've been hiring mathematicians to verify this stuff themselves. They're obviously not just throwing it out there without any human review.

And these mathematicians sink the comment to the bottom in 5 min?

It is not peer review if it is all in one company that wants an IPO.