3 ms·

> checking an existing fully fleshed out proof is simple The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.

• akoboldfrying 3mo ago
  How does this involve computer checking of a formal proof? 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.
• pfdietz 3mo ago
  His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed. This is one of the great things about formalization: it would have avoided this entire debacle.
  • bsder 3mo ago
    > 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.
    • pfdietz 3mo ago
      > It's also a MASSIVE amount of SUPER TEDIOUS work. 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.