> Acceptance of the work in Publications of the Research Institute for Mathematical Sciences (RIMS) — a journal of which Mochizuki is chief editor, published by the institute where he works at Kyoto University
> Mathematicians often publish papers in journals where they are editors. As long as the authors recuse themselves from the peer-review process “such a case is not a violation of any rule, and is common”, says Hiraku Nakajima, a mathematician at the Kavli Institute for the Physics and Mathematics of the Universe in Tokyo formerly part of Publications of RIMS’s editorial board. Mehrmann confirms that this would not violate EMS guidelines.
> Kashiwara said that Mochizuki had recused himself from the review process, and had not attended any of the editorial board meetings about the paper. The journal has previously published papers from other members of the journals’ editorial board, he said.
Speaking as someone who used to make a living by publishing (though not in mathematics): the problem with this is that even though you may have recused yourself, everyone who is still in the room knows that you will be passing judgement on their papers at some point in the future. So recusal does not entirely remove the potential for conflict of interest.
I agree, not necessarily because publishing in a journal one is involved in is uncommon, but rather because putting one's work there although this work is disputed in the community clearly signals that one has not managed to build consensus and does not want/is not able to fight the good fight. If it was an incremental addition to well-established work that hardly anyone in the community can dispute, it would be a different story.
It would also be extremely strange to publish a result like a proof of the ABC conjecture in a third-tier journal where you are an editor (actually, the editor-in-chief) rather than a top-tier journal.
TL;DR: obscure, long "proof" of major conjecture by respected mathematician to be published in a journal he is closely associated with despite several years of scepticism by the wider maths community his attempt is successful.
Complicated somewhat by possible language and cultural barriers, and his perceived reluctance to fully engage with his critics or the maths world outside his home country.
It's an interesting and odd story that has been rumbling on for the last few years.
Although if you look at his rather colourful webpage, the strong, almost defensive, warning that Japanese will be the language used (at a Japanese institution of course) doesn't detract from the anecdotal suggestions that have dogged the saga of a reluctance to engage more fully with the world beyond his local region.
I'm not argusing that he's not cagey. Simply that there is no issues of a language barrier (instruction in Japanese at Japanese university is a complete red herring when talking about what language he engages with the international mathematical community in).
I would be pissed too if I were a professor and some undergrads insisted on speaking about mathematics to me in Japanese simply because they view it as a "lingua franca". The argument that "English is the lingua franca" is akin to "let's use Electron because web is the most cross-platform".
That is true. It is sometimes annoying that English speakers so often never tries to learn a new language and just expects everyone else to use theirs.
However, one could view it as the only common language between you and someone else and use it for that reason. In my mind the one that know more languages are able to more easily communicate with more people more accurately, and as such have a leg up on teaching and learning from others. These ideas might be able to travel faster since they can travel by English and Japanese. Though maybe that is just wishful thinking from my side.
In my experience monolingual people underestimate the effort it takes to use your non-dominant language(s). For example, I could theoretically communicate in Spanish, but the effort it takes to deal with romance language conjugation is a legitimately unpleasant experience for me. Mochizuki might know English, but it might be the case that using it is an unpleasant experience to him. In addition, just as there are English proficiency requirements for international students in the US, I feel it would be unreasonable to pursue higher education in Japan without even knowing enough Japanese to talk about math.
I agree. I'm just noting a certain pre-emptive antsiness there that is consistent with the allegedly defensive tone of his general approach to engagement with his peers.
Of course, it could be coincidental, and he could also have been unfairly represented in his willingness to engage.
If the TLDR is long enough to include that it's in a journal the author was associated with then it's long enough to also mention that this isn't an abnormal thing in mathematics. Otherwise both details should be excluded.
Yes, but is it normal for a work of such importance by a mathematician so respected (which would presumably have publications fighting for it) to be apparently publishable - especially after such contention as to its validity - only in a journal he is associated with? And let's be clear, by "associated with", we mean chief editor.
I was actually careful to exclude that particular job title from my OP to avoid the unfairness you are implying in my initial summary.
However, your point is correct in ordinary situations. This is no ordinary situation.
Math student here. This whole process reflects very poorly on Mochizuki, IMO. The proper thing to do when claiming to have solved a major open problem is to make yourself available to the mathematical community, for example by giving lectures on your work. Releasing a preprint on your website and expecting other mathematicians to drop what they're doing and devote years of their time to understand your obscure paper just screams of arrogance. Also, publishing your work in a journal where you are the editor isn't a good look; it gives the impression of a conflict of interest. The critique by Scholze et al is the final nail in the coffin as far as I'm concerned.
Thanks for this. Tao’s comment made quite an impression on me, but important for outsiders like me to remember that the facts on the ground can change as time goes on.
To quote, "To take an extreme example, if Mochizuki had carved his argument on slate in Linear A and then dropped it into the Mariana Trench, then there would be little doubt that asking about the veracity of the argument would be beside the point. The reality, however, is that this description is not so far from the truth."
The real problem is that his response to Scholze and Stix didn’t manage to convince anyone who wasn’t already in his camp. At this point there is a major and clearly stated objection to the proof out in public to which no reasonable refutation has been offered.
> At this point there is a major and clearly stated objection to the proof out in public to which no reasonable refutation has been offered.
The problem is: Scholze and Stix formulated their objections to a "simplified" version of IUTT (i.e. they did quite some identifications). Their claim is that these simplifcations do not matter for whether IUTT holds or not, but Mochizuki claims that the details that Scholze and Stix "wiped away" do matter. No side could convince the other side of their position.
He didn't give his two biggest critics the time of day. You can't fault them for sticking to their conclusion, the authority to the contrary is completely uninterested in defending their position.
We'll probably never know if he actually solved it. Few have the knowledge, fewer had the patience and nobody has had rebuttal. Scholze and Stix conclusions hold exactly as much weight as Mochizuki's. They are unwilling to change their mind and recant, just as much as Mochizuki is.
This whole fiasco reflects very poorly on the mathematical community in general.
> But one mathematician who prefers to be quoted anonymously says that editors and referees handling these papers might have been in a nearly impossible situation. “If the best mathematicians spend time trying to work out what’s going on and fail, how can one referee on his own have any chance?”
I totally disagree. When someone is making extraordinary claims, the burden is on them to go the extra mile to explain their reasoning, none of which Mochizuki has done. The easy decision in this case should be to leave things at the current "default" state unless a higher burden of proof is met.
I think it reflects especially poorly that when confronted with criticisms that Mochizuki just waved the criticisms away with what was basically a "you mere mortals misunderstood my greatness", without taking the effort to engage and explain himself. I'm not in the math community so could be misunderstanding, but that's certainly the sense I got reading this article.
They go the extra mile to explain it to other experts. When Perelman produced his proof of the Poincare conjecture, he traveled all over the place explaining his result.
> It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
This seems like the crux of the controversy: what is the true value in the 300+ "pages of set up"? Clearly he's providing a new framing for the problem. If that new framing ends up being applicable to other problems (which was presumably the author's intent), then the "pages of set up" are the true value here, not the proof of the abc conjecture itself.
When Tao says, "no smaller fragment of this setup having any non-trivial external consequence whatsoever"—this is a comment about the state of things so far—but whether that will change is unknown.
Maybe all of that "set up" ends up having no more general utility whatsoever, or maybe we shouldn't even expect to have found external consequences yet: very fundamental re-framings may be very disconnected from applications. Maybe Mochizuki has found one path from the new framing back into an area of contemporary mathematical interest, and maybe further exploration will yield an abundance of new paths—maybe some highways.
Anyway just playing devil's advocate since the prevailing stance on this seems to be against Mochizuki in a way that feels odd to me.
I'm not a mathematician but coming from the software world if one guy wrote a massive program (I'm assuming 600 pages is massive) in "an impenetrable, idiosyncratic style" you could virtually guarantee it would not be correct.
Surely not the best example, but Terry A. Davis' (RIP) TempleOS was written in a very idiosyncratic style (he even invented his own programming language (HolyC) for this).
Being able to mix text, images, 3d models, etc in a terminal session is something that modern OSes still haven't gotten around to doing. Terry may have been crazy but he was right about a lot of things and unlike many, he had the skills to implement his ideas
It definitely poses a challenge to the question of what a mathematical proof actually is. One of the things about mathematics is in a way its 'obviousness', there's a way in which once something is proven its intelligble to mathematicians in an immediate, direct sense.
A 600 page proof that requires essentially a new branch of idiosyncratic mathematics which as an end result is barely understandable even by peers in the field almost moves it from mathematics into the realm of empirical science, where people are often for years occupied with interpretation of data and discussions about how significant a finding is.
As mathematics moves on to tackle more and more complicated questions I think it's interesting to ask if there will be a push back against complicated solutions, focus on simplicity as integral to solving a mathematical problem, and so on.
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.
> 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
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.
I would expect the base axioms to be specified by the author of the paper. That is, by the guy who claims to understand it.
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.
The problem is that the base "axioms" (really, definitions) he's working off of are basically alien language, and almost nobody understands why they are relevant. Add to that he is not saying "turn the crank like this", but is effectively saying "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".
On the other hand, there was a similar case with a German mathematician beforehand, and he turned out to be correct.
I don't buy that the base axioms are alien and it doesn't matter anyway.
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)
Not a mathematician, but I've kept up with this story as a non-mathematician.
> 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.
There are theorems like that. (The classification of finite simple groups, whose proof is famously thousands of pages long, is like that.) But Mochizuki's proof is not like that. He creates a lot of definitions, and it's hard to figure out what the content of the definitions are.
The comment from "PS" and the reply from "BCnrd" on this blog post https://www.galoisrepresentations.com/2017/12/17/the-abc-con... (which was linked elsewhere in this comment section) claim, more or less, that there are 49 lemmas which are presented in sufficient detail to be computer-checkable, and one lemma which is not presented in enough detail for either computers or (most) humans to check, but is stated to follow straightforwardly if you understand the overall argument made by the other 49 lemmas. There are a couple of people besides Mochizuki who say "Yes, it does follow immediately, it's pretty clear," and they haven't been able to communicate why it's pretty clear to anyone else.
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
Once again, this is a rather perfect example of why there is a great need in Math for a universal formal proof language that can be verified by computers.
If this existed, the burden of proof would be on Mochizuki to present his proof in a language that can actually be understood by others and by machines.
The problem is that producing a formal proof that can be verified by a computer is incredibly boring. Since it's incredibly boring, nobody is going to do it. It's not a matter of a universal formal proof language existing (there are lots of frameworks that are powerful enough), it's matter of one being easy enough to use that people will willingly use it.
Well, suppose you want to prove another result similar to abc conjecture. What would you rather read, a formal proof (basically low-level machine code), or an actual human description of a theory used to produce the result?
What would need to exist to make such a proof specification utility less boring? I know many engineers who never thought they'd use unit tests until I was able to demonstrate immediate workflow benefit that made their job far easier than before. If you have experience in higher math, what would need to exist to make such specification useful?
The challenge is making a tool that's sufficiently ergonomic. It's the UI problem from hell. The problem is that people are much smarter than computers, so you can just specify the broad strokes and your audience can fill in the details as needed.
For starters, it would be nice to be able to make trivial manipulations of algebraic expressions involving real numbers not incredibly tedious. As far as I know no existing proof assistant is up to that challenge. Again, it's not a matter of power--many, many proof assistants can formalize the vast majority of mathematics--it's about UX.
Category theory depends on set theory. Unluckily, formulating a category of all sets/groups/rings/... is not easy because there exists no "set of all sets/groups/rings/...".
One way to solve this problem is to replace ZFC by its non-conservative extension Tarski–Grothendieck set theory
Most of category theory as used in ordinary mathematics can be formulated in ZFC. The category of all groups, etc. is just a propositional formula. If you prefer to explicitly talk about classes, then you can go with NBG, which is a conservative extension of ZFC.
It seems mathematicians are not aware of code obfuscation. Mochizuki objective is to keep this knowledge in Japan and protect this technological advantage.
Weird, why? Since he can't keep this information from leaking around the world, the best strategy is to obfuscate it and show his trusted partners the concepts required to understand it. By gaining notoriety around the world, he is also attracting more partners, and he can filter them out (ie. he knows english, but will only do lectures in japanese, inside the country). If at some point the information gets fully decoded, he will be recognized as having solved the problem anyway. In the meanwhile there is a technological advantage to keep.
What is the technological advantage of proving the ABC conjecture? Seems like any application for it would comparatively take much more time to develop than whatever time advantage can be gained through obsfucation.
As far (though little) as I know, that's way beyond feasible still -- lean has a ton I think, but is nowhere near covering the "seam" of mathematics -- many fundamental objects are not even defined themselves yet, so you'd have to do lots of extra work there, not to mention all the work to define your own new things.
Lean is amazing (and I played around with it a bit, should do so more) but I don't suspect it's realistic to expect new theorems of this magnitude to be written in it at this point yet, doing so is a huge huge effort on top of the life-altering effort that the theorem itself requires.
Although he had lived in the US for more than a decade and has no problem with the English language, he seem to have a kind of "western culture allergy" that is written in detail in the post below:
"The saga began when Mochizuki, a respected number theorist quietly posted his preprints on 30 August 2012 — not on arXiv.org, mathematicians’ preferred repository, but on his own webpage at RIMS. Written in an impenetrable, idiosyncratic style, the papers seemed to entirely consist of mathematical concepts that were completely unfamiliar to the rest of the community —
“like you might be reading a paper from the future, or from outer space”,
wrote Jordan Ellenberg, a number theorist at the University of Wisconsin–Madison, on his blog soon after the papers appeared."
...Which makes it all the more a subject of curiousity -- and worth looking at...
The top 2 math journals are, in many people's minds, Annals and Inventiones (i.e. Annals of Mathematics and Inventiones Mathematicae). The fact that this work, which is supposed to be of utmost importance, was not published in one of these two, is not confidence inspiring. That it was published in a journal where the author is chief editor is downright scandalous.
89 comments
[ 3.0 ms ] story [ 137 ms ] threadThat's exceptionally bad optics.
> Mathematicians often publish papers in journals where they are editors. As long as the authors recuse themselves from the peer-review process “such a case is not a violation of any rule, and is common”, says Hiraku Nakajima, a mathematician at the Kavli Institute for the Physics and Mathematics of the Universe in Tokyo formerly part of Publications of RIMS’s editorial board. Mehrmann confirms that this would not violate EMS guidelines.
> Kashiwara said that Mochizuki had recused himself from the review process, and had not attended any of the editorial board meetings about the paper. The journal has previously published papers from other members of the journals’ editorial board, he said.
Complicated somewhat by possible language and cultural barriers, and his perceived reluctance to fully engage with his critics or the maths world outside his home country.
It's an interesting and odd story that has been rumbling on for the last few years.
Scholze and Stix had to go to him.
http://www.kurims.kyoto-u.ac.jp/~motizuki/students-english.h...
However, one could view it as the only common language between you and someone else and use it for that reason. In my mind the one that know more languages are able to more easily communicate with more people more accurately, and as such have a leg up on teaching and learning from others. These ideas might be able to travel faster since they can travel by English and Japanese. Though maybe that is just wishful thinking from my side.
Of course, it could be coincidental, and he could also have been unfairly represented in his willingness to engage.
I was actually careful to exclude that particular job title from my OP to avoid the unfairness you are implying in my initial summary.
However, your point is correct in ordinary situations. This is no ordinary situation.
Here are some texts from the internet concerning this:
David Michael Roberts - A Crisis of Identification: https://inference-review.com/article/a-crisis-of-identificat...
Two Quora posts:
https://www.quora.com/Did-Peter-Scholze-and-Jakob-Stix-reall...
https://www.quora.com/What-do-you-think-about-Stix-and-Schol...
Also relevant:
https://thehighergeometer.wordpress.com/2019/01/18/taylor-du...
The problem is: Scholze and Stix formulated their objections to a "simplified" version of IUTT (i.e. they did quite some identifications). Their claim is that these simplifcations do not matter for whether IUTT holds or not, but Mochizuki claims that the details that Scholze and Stix "wiped away" do matter. No side could convince the other side of their position.
If you want to dive into the gory details:
http://www.kurims.kyoto-u.ac.jp/~motizuki/SS2018-08.pdf (Scholze & Stix)
http://www.kurims.kyoto-u.ac.jp/~motizuki/Rpt2018.pdf (Mochizuki)
If you love flamewars, read: Ivan Fesenko: Remarks on Aspects of Modern Pioneering Mathematical Resarch; https://www.maths.nottingham.ac.uk/plp/pmzibf/rapm.pdf
We'll probably never know if he actually solved it. Few have the knowledge, fewer had the patience and nobody has had rebuttal. Scholze and Stix conclusions hold exactly as much weight as Mochizuki's. They are unwilling to change their mind and recant, just as much as Mochizuki is.
This whole fiasco reflects very poorly on the mathematical community in general.
http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTch-discussions-...
It's worse than that. At this point, the person who bridges that gap will almost certainly get his name added to the proof--that's a big incentive.
The fact that nobody seems to be able to bridge that gap is a gigantic glaring flag that something is wrong.
Taylor Dupuy together with Anton Hilado is attempting this:
https://thehighergeometer.wordpress.com/2019/01/18/taylor-du...
This isn't something you hype like a iPhone.
I totally disagree. When someone is making extraordinary claims, the burden is on them to go the extra mile to explain their reasoning, none of which Mochizuki has done. The easy decision in this case should be to leave things at the current "default" state unless a higher burden of proof is met.
I think it reflects especially poorly that when confronted with criticisms that Mochizuki just waved the criticisms away with what was basically a "you mere mortals misunderstood my greatness", without taking the effort to engage and explain himself. I'm not in the math community so could be misunderstanding, but that's certainly the sense I got reading this article.
that’s not how extraordinary math worked in the past
> It seems bizarre to me that there would be an entire self-contained theory whose only external application is to prove the abc conjecture after 300+ pages of set up, with no smaller fragment of this setup having any non-trivial external consequence whatsoever.
This seems like the crux of the controversy: what is the true value in the 300+ "pages of set up"? Clearly he's providing a new framing for the problem. If that new framing ends up being applicable to other problems (which was presumably the author's intent), then the "pages of set up" are the true value here, not the proof of the abc conjecture itself.
When Tao says, "no smaller fragment of this setup having any non-trivial external consequence whatsoever"—this is a comment about the state of things so far—but whether that will change is unknown.
Maybe all of that "set up" ends up having no more general utility whatsoever, or maybe we shouldn't even expect to have found external consequences yet: very fundamental re-framings may be very disconnected from applications. Maybe Mochizuki has found one path from the new framing back into an area of contemporary mathematical interest, and maybe further exploration will yield an abundance of new paths—maybe some highways.
Anyway just playing devil's advocate since the prevailing stance on this seems to be against Mochizuki in a way that feels odd to me.
Being able to mix text, images, 3d models, etc in a terminal session is something that modern OSes still haven't gotten around to doing. Terry may have been crazy but he was right about a lot of things and unlike many, he had the skills to implement his ideas
A 600 page proof that requires essentially a new branch of idiosyncratic mathematics which as an end result is barely understandable even by peers in the field almost moves it from mathematics into the realm of empirical science, where people are often for years occupied with interpretation of data and discussions about how significant a finding is.
As mathematics moves on to tackle more and more complicated questions I think it's interesting to ask if there will be a push back against complicated solutions, focus on simplicity as integral to solving a mathematical problem, and so on.
Contrast with Wiles, where they _did_ understand it, they _did_ find a gap in his proof and he fixed it to everyone’s satisfaction.
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.
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?
> 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...
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
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
If this existed, the burden of proof would be on Mochizuki to present his proof in a language that can actually be understood by others and by machines.
One can't help but wonder: as boring as reading through inter-universal teichmuller theory?
So, I believe that this would make it highly complicated to even formulate some very new math at the borderlands of our knowledge.
One way to solve this problem is to replace ZFC by its non-conservative extension Tarski–Grothendieck set theory
https://en.wikipedia.org/w/index.php?title=Tarski%E2%80%93Gr...
to ensure that a Grothendieck universe
https://en.wikipedia.org/w/index.php?title=Grothendieck_univ...
always exists.
Grothendieck needed an extra axiom because he wanted to consider large Grothendieck topologies. The consensus seems to be that universes are avoidable: https://mathoverflow.net/questions/35746/inaccessible-cardin...
Lean is amazing (and I played around with it a bit, should do so more) but I don't suspect it's realistic to expect new theorems of this magnitude to be written in it at this point yet, doing so is a huge huge effort on top of the life-altering effort that the theorem itself requires.
https://www.maths.nottingham.ac.uk/plp/pmzibf/rpp.pdf
https://plaza.rakuten.co.jp/shinichi0329/diary/202001050000/
Although he had lived in the US for more than a decade and has no problem with the English language, he seem to have a kind of "western culture allergy" that is written in detail in the post below:
https://plaza.rakuten.co.jp/shinichi0329/diary/201711210000/
I think the "allergy thing" is the reason he doesn't want to follow the ordinary "western approved way" and do a tour in the US.
Also I have read somewhere that he is open to mathematical discussions via online or if you visit him in Japan.
"The saga began when Mochizuki, a respected number theorist quietly posted his preprints on 30 August 2012 — not on arXiv.org, mathematicians’ preferred repository, but on his own webpage at RIMS. Written in an impenetrable, idiosyncratic style, the papers seemed to entirely consist of mathematical concepts that were completely unfamiliar to the rest of the community —
“like you might be reading a paper from the future, or from outer space”,
wrote Jordan Ellenberg, a number theorist at the University of Wisconsin–Madison, on his blog soon after the papers appeared."
...Which makes it all the more a subject of curiousity -- and worth looking at...