A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the truth of which has already been established. So while coming up with a proof may require genius-level thinking, checking an existing fully fleshed out proof is simple -- just potentially very tedious because of the sheer number of steps.

That said, a typical human-written proof omits many steps considered "obvious" to a trained mathematician. Converting this to a formal proof involves interpreting what the original author "must have meant", which requires a lot of expertise and can go wrong -- or it may reveal that there is some inconsistency in the original claim itself.

The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.

Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs.

ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.

This is one of the great things about formalization: it would have avoided this entire debacle.

It's also a MASSIVE amount of SUPER TEDIOUS work. And it's the kind of work that folks who think up advanced math proofs tend to loathe. It's along the lines of programming by toggling in the code from front panel switches.

So what current mathematics does is judge a proof by whether or not the application of the proof somehow coincides with the result from some other adjacent branch of mathematical knowledge. So, a "novel" proof is expected to either help prove something in a slightly different branch of mathematics or simplify some already existing proof.

And that is, as I understand it, the crux of the matter with the Mochizuki proof of the "abc Conjecture." Solving the "abc Conjecture" should provide tools for solving other similar problems just like Wiles' proof of Fermat's Last Theorem provided an entire class of tools for dealing with modularity and elliptic curves. And yet Mochizuki seems to unable to do or demonstrate any of that.

So, Mochizuki's work is like someone dropping a gigantic and impenetrable proof of exactly and only Fermat's Last Theorem that doesn't apply to anything else. Sure, it would be an interesting (and true!) thing, but without the ability to use it further, it's a curiosity rather than a pillar.

It was, but now autoformalization is a thing. If he had delivered his proof and a formalization -- no matter how much it looked like autogenerated slop -- he would have been taken much more seriously.

Despite reluctance to do formalization, I expect it will gradually become required to get math published, since journals will be flooded with AI generated slop. It will be necessary to filter the slop, and requirement of formalization in the supplementary material would be a good way to do that. It would still be necessary to check that the formalization of the statement of the theorem is correct, but that's a much smaller ask.

But I also definitely don't understand the problem if I can't get the computer to understand it, with tests.

In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.

With all of these questions in the air, epistemology might be making a comeback.

I disagree, software engineering is a mature discipline now, and at this point we have so many testing frameworks (unit testing, syntax testing, regression testing, fuzzing, testing end to end, live, with a subset of known good and incorrect inputs, chaos monkeys, etc, etc, that to say "there's no way of verifying the AI-generated code" is frankly incorrect.

Or, if you insist, defend the "there's no way of verifying the code, at all", and not only AI-generated.

(if it helps I work in the company where before the code even starts being written, several extensive tests for it must be ready first. It's hard to even commit a broken code, and later in the pipeline it's very easy to catch the subtly broken or incorrect code)

Type theory can also be an independent synthetic foundation atop which you build mathematics.

Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.

No.