Abhyankar and others spent years trying to find an easier proof. I’m not an algebraic geometer and I don’t know the state of things now. I was under the impression that on the level of Ideals, Varieties, and Algorithms one can introduce the concept and do some calculations but not present a proof of the theorem.

But the point is that pre-AI it was already the case that famous results were published that very few could understand or digest. I think it is reasonable to expect that we will soon be at a point that Lean says a theorem is correct but no human can or will ever understand the proof.

What if Lean verifies Mochizuki’s proof of the ABC conjecture. Do we disregard it becuase no other mathematician understands the proof?