Mochizuki proof of abc conjecture

Stream: Is there code for X?

[Lars Ericson]

I'm just throwing this out there. Checking this proof would be a beautiful application of Lean: https://www.sciencealert.com/600-page-mathematical-proof-is-about-to-be-published-other-mathematicians-aren-t-impressed

[Patrick Massot]

This has been discussed countless times before. Unfortunately there is to check there.

[Kevin Buzzard]

As has been said many times before, the 600 pages are not yet in a state where they can be checked by Lean because humans don't understand them.