[deadbeef57]

As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being.

The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).

[kungito]

What's the name of this point? It's really hard to find any progress on this topic regarding Mochizuki other than some popular articles without any content.

[deadbeef57]

See https://www.math.columbia.edu/~woit/wordpress/?p=10560, which links to a technical write-up by Scholze and Stix about what they think is the issue with Mochizuki's proof. Woit's blogpost also gives a bit more links, including a response by Mochizuki.

[bryan0]

The paper which everyone linked to when the discussion was going on now 404s, so here is a new link: https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...

The point in the proof where scholze and stix show it fails is “IUTT-3, Corollary 3.12”