I don't have any idea what this proof looks like and I can assume it's very complex. But, could it be modular enough that you can check the proof without understanding it?
For instance, imagine the proof is made of 50 lemmas. One could check the main theorem derives from the 50 lemmas. And checking each individual lemma could be left to other mathematicians.
> For instance, imagine the proof is made of 50 lemmas. One could check the main theorem derives from the 50 lemmas. And checking each individual lemma could be left to other mathematicians.
To my understanding, some mathematicians have gone ever further and checked the work themselves. Peter Scholze (a 32-year-old who won the Fields medal a couple of years ago and seems to be in the sweet spot of expertise and stamina to really audit this thing) has identified a specific result ("Corollary 3.12") that he says does not follow from the results leading up to it [1]. This is pretty weird because "Corollary" is usually reserved for things that are immediate consequences of previous results.
Based on the featured article, Scholze's position hasn't changed. There is a specific objection and the two sides just...disagree.
For those interested, you can look at the papers yourself if you want to. Here's the one containing the controversial result [2]. Theorem 3.11 is on p153, and the statement alone is 5 pages long. The proof is 3 lines and asserts that it's obvious from definitions and previous statements. Corollary 3.12 is on p173.
As an outsider, I am amazed at Scholze's ability to work through all of this and identify a specific criticism.
[1] https://inference-review.com/article/a-crisis-of-identificat...
[2] http://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20...
IANAM, but formalizing mathematical proofs that they can be machine-checked is hard, tedious and I guess doesn't get you much fame either. Doing this for such a monstrosity of proof must be an epic task.
And as far as non-machine-checked analysis goes, other mathematicians have claimed that specific parts contain flaws (TFA mentions this) but the author disagrees.
Despite multiple conferences dedicated to explicating Mochizuki’s proof, number theorists have struggled to come to grips with its underlying ideas. His series of papers, which total more than 500 pages, are written in an impenetrable style, and refer back to a further 500 pages or so of previous work by Mochizuki, creating what one mathematician, Brian Conrad of Stanford University, has called “a sense of infinite regress.”
It’s not possible to “check the main theorem derives from the 50 lemmas” if each of the lemmas uses terminology one doesn’t understand or even has never heard of.
After that the steps of the proof should be just turning the handle, and perhaps the distance between steps to be bridged automatically. Maybe you wouldn't understand what was going on and likely not understand the end product any better but at least by symbol manipulation alone you should be able to make a path and verify that start via steps arrives at conclusion
Of course I am not a mathematician and haven't a clue but in principle it seems viable and if it isn't I'd really love to know why.
On the other hand, there was a similar case with a German mathematician beforehand, and he turned out to be correct.
I can give you an alien language of logical axioms, and a series of steps, none of which a random person wouldn't be able to understand, but could still lead them through a series of steps, showing that the outcome could be derived from the input via the axioms.
Now, if nobody could understand the axioms and steps of this but they still got a consistent outcome, mathematicians would still be interested if for no other reason than it was self-consistent. That alone would be a result.
But if they had that, I suspect that would also give them a framework for understanding it.
> "trust me when I say the cranks turn and out pops the answer, but if you dig into the machinery yourselves you'll see what I mean".
automate that and there'll be no need to trust him.
And those are papers that an expert can skim to get an idea about the flow of the proofs. This one, if you jump in, says you things like “every fooable bazz is a bar”, where foo, bar and baz are new terms no mathematician has any intuition for that, likely, got defined in terms of other hitherto unknown terms qux, quux and quuz, making it impossible to judge whether that statement has merit, or how it leads to proving the abc conjecture.
And yes, an automated proof checker would be nice to have, but we aren’t there yet, by a wide margin. Getting there would make this proof a lot longer.
(For a loose analogue: imagine that the published solution to a “mate in 2” problem in chess wouldn’t just be “Queen g1, check, King h8, rook h2, mate”, but “whites queen is on field d1, by rule r queen can move horizontally across empty fields, there are no empty fields between d1 and g1, that doesn’t bring white’s king in check (blacks pawn on e4 can’t take it because…, blacks knight on c6 can only move to… because of rules…, so white can move their queen to g1. That brings black in check because of rules…, etc)
Who is that?
That was in 2017: in 2018, Peter Scholze and Jakob Stix spent a week with Mochizuki trying to understand the proof and published their claim that the proof is flawed, which focuses on that very same unclear portion. In their understanding, that portion of the proof claims something much weaker and uninteresting, and they haven't been convinced of the intended claim. http://www.kurims.kyoto-u.ac.jp/~motizuki/SS2018-08.pdf