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).

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.

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.

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”

Made an account just to share this incredible book that follows Erdos's life & exploits:

https://en.wikipedia.org/wiki/The_Man_Who_Loved_Only_Numbers

On the contrary proof assistants help one systematize and organize existing concepts. They are a great way to revise the basic curriculum and revolutize pedagogy. They make the creative process of defining new mathematical objects more accessible, and easier to motivate via unlocking more code reuse. They are a great way to revise the basic curriculum and revolutize pedagogy.

I strongly agree on this one. As a programmer and someone who's always been interested in mathematics, having a way to check proofs without relying on trust of my own logic or a third agent, but solely on a prover like Lean or Coq is a really big difference.

Automated proofs aren't remotely comparable to Mochizuki's abc stuff. Automated proofs just handle a lot of complicated case by case checking that humans could in principle do, it's just too much work, like counting to a trillion. Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.

Mochizuki's stuff is simply a hypercomplicated pile of nonsense unintelligible to the mathematical community.

> Automated proof systems are incapable of the brilliant but unreliable intuitive leaps that mathematicians can make.

I would add current automated proof systems. IMHO we are just at the beginning that mathematicians realize the usefulness of technology, which was basically neglected ever since.

It will be very interesting to see what happens! A common theme in mathematics is that the proofs are the (relatively) easy part, while knowing what to prove is hard. Still, I'm sure mathematicians will welcome greater automation of the "easy" part. If machines ever do more than drudge work, there will also be the challenge of making the machine-generated proofs intelligible to humans, similar to the interpretability issues around machine learning models today.

> but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics

Related to the unexplainability of AI. We're just grasping for more than we can hold in our little working memory.