- An error was found in 2012 and was just recently (Nov 2014) corrected
- He's re-released his notes & lectures on the subject
- A workshop will be held on the topic in March
That doesn't seem to be unusual / isolationist behavior, though it's obviously a complicated topic and since Fermat's Last Theorem has been deemed 'solved' already, the fact that it makes a FLT proof easier isn't much appreciated by the press / community.
No doubt the guy's exceptionally brilliant, and perhaps one day a mathematician with enough motivation to do it will spend a very long time trying to understand and decipher what he constructed, but my take on it is that anyone that wants to communicate a message, no matter how brilliant, should also go to the trouble of making it as legible as possible to others.
This is actually a major gripe of mine when reading papers - not enough effort to communicate the math so it's readable. It's really frustrating to decipher a paper when there's a lot of hand waving. It's 10x worse when buzzwords or unimportant relationships are also included.
If you've gone through paper-publishing, editors ask for pretty large reductions. A 29 page paper can easily be a 50-60 pages paper with "decent details" or a 150 pages paper with clear explanations of all details.
This assumes infinite time to add all minutiae to LaTeX. Not everyone works directly on that, almost everyone thinks on paper, develops ideas on paper and then TeXifies it. In my case, most of the "it is clear that" never made it into any version of the final file.
Well, you certainly don't need all the minutiae, but some hand holding, especially on specific papers that deal with some theorems that might not be so well know would be helpful.
My favorite journal - the electronic journal of combinatorics - doesn't have page limits because it never gets printed. You can also use as many colors as you like in your diagrams!
Meanwhile, a friend of mine uses a bool in their LaTeX files for 'idiot mode'; flip it on and recompile to get the painfully detailed versions of all the proofs. Since the source is on the arxiv, it means each paper has a kind of half-hidden long version.
I've been working on a paper from my PhD thesis. I have 10 pages of derivations before I even get to the solution of the equations, include figures, or perform analysis. It could easily be a 30 to 40 page paper. Cutting it down or splitting it into 2 papers will likely be necessary because of page limits. You kind of need to pick and choose what to leave out.
Of course, it happens without page limits as well. I used work from an older book and between two steps was easily two pages of work and there's another half dozen pages of work that from other parts of the derivation.
I have been seeing this too. Steve Pinker in his books, Sense of Style, has portions which talk about this problem. He calls it -"Curse of Knowledge" and has advise for scientific writers. I wish researchers could spend a bit more time on improving their writing skills for better communication.
Beyond the paper constraints, there's often something of a selective pressure to obfuscate as a way to get through review. Math you don't quite understand seems complex. Math that's clear and concise seems, after the fact, to be trivial.
I read the report linked in the article and Mochizuki et al do not seem to think that studying this would take prohibitively long time. Some select quotes:
> During these lectures, Yamashita warned that if you attempt to study IUTeich by skimming corners and “occasionally nibbling” on various portions of the theory, then you will not be able to understand the theory even in 10 years; on the other hand, if you study the theory systematically from the beginning, then you should be able to understand it in roughly half a year.
> Unfortunately, however, there appear to exist, especially among researchers outside Japan, quite strongly negative opinions and antagonistic reactions to the idea of “studying the theory carefully and systematically from the beginning”.
>From the point of view of achieving an effective solution to this sort of problem [=education], the most essential stumbling block lies not so much in the need for the acquisition of new knowledge, but rather in the need for researchers (i.e., who encounter substantial difficulties in their study of IUTeich and related topics) to deactivate the thought patterns that they have installed in their brains and taken for granted for so many years and then to start afresh, that is to say, to revert to a mindset that relies only on primitive logical reasoning, in the style of a student or a novice to a subject.
If it's in your interest that I understand what you're saying, and you make it too hard for me to parse your stuff down to a comprehensible level - then it's your fault, not mine.
He did the entire 500-page paper in isolation and refuses to lecture on it in any capacity anywhere other than his own university. He may be right, and he may not be, but his failure to get an answer from the community is his fault, not theirs.
Minhyong Kim (cited from the article) makes a good point: that "any journal would probably require independent reviewers who have not studied under Mochizuki to verify the proof."
Given that, Mochizuki is stuck between a rock and a hard place - anyone he brings up to speed automatically becomes disqualified to independently review his work.
While you're correct, part of the fix for that is not to publish a 500-page paper in isolation. You instead publish the underlying concepts piecemeal in "easy"-to-understand chunks (for this insane level of "easy", hence the quotes). This works the same as how good practice when writing code is not to drop a 50 ksloc commit, but rather to do a series of patches showing how you arrived at a given solution.
My friends and I occasionally joke that the worse a professor's/programmer's/scientist's personal university webpage, the better they are at their actual profession.
It's not the worse mathematician homepage I've seen, by a grand margin. Mine is only marginally better, and I have more to blame since I know what I do when I do webpages :)
When I was in academia, I just used Word (and "Export to HTML") to create my university homepage. Even back then, I knew it was ugly as sin, but I had other things to worry about.
I still don't have a very good sense of design, but I can use Bootstrap. That's good enough.
did you look at the source, that was written by a mathematician, he took careful care to calculate out every pixel of padding and space. Probably for his specific monitor :)
> If nobody understands a mathematical proof, does it count?
Nope. That's the social aspect of mathematics: your proofs have to be comprehensible and considered to be correct by those in the mathematical community that read them (at least peer review) before they're accepted.
A professor once defined a proof as "That which is convincing", and we were free to say, "I am not convinced"
While the topic being proven may be technically correct, the act of proving is a social act. The formal notation just makes this more precise than human language.
Proof is "that which is convincing to a fair and rational mind." It should compel a rational actor into the verifiable mitigation of some risk.
This particular fuss is one of the side effects of mathematicians' failing to properly adopt computers into their process. One of these days we will not accept a proof unless it is computer verified, and there will be no social aspect to it.
It should not matter if your proof is 10,000 pages if a computer can follow it.
It is still better to have a clean 1-page proof. There is no direct value for proving a theorem. Mathematics is nice because it's useful for further mathematics, useful for real-world applications, and beautiful. A 10,000 page proof that only a computer can follow is none of these things.
It is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms.
So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
> surely there exist useful proofs that require 10,000 pages minimum
The classification of finite simple groups "consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."[1]
That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. What you can't do is compress _all_ proofs to single-sentence proofs using a finite number of unique symbols.
We know that a computer can't verify all unknowable theorems. (Theory of Computation) But perhaps one can verify all provable theorems.
I suspect that computers will struggle on the cleverness factor, where proof requires joining multiple fields of math, rather than just running through algebraic manipulation.
Could a computer verify that the domino problem is undecidable? The proof consists of translating the problem into non-halting universal turing machines.
There's also a luck aspect. Perhaps Mochizuki's proof is comprehensible but no one has the desire to read it. A mathematician or scientist should be prepared to be a lone wolf, never receiving recognition and their groundbreaking ideas never known to another.
Hopefully someday, model checkers and proof assistants can help mathematicians to put these monster proofs into format that can be verified with computer.
When I was a student, I started making such a system. It would also be very beneficial for students for explaining complex proofs.
The main problem is not in model checker (there are plenty of them already), but to automatically convert between a model checker syntax (that looks rather like a programming language), and regular math paper syntax (which is free-form English, so you need general AI for reading that).
I was already quite experienced programmer at that time, but realized the UI/UX problem is too big for me alone, even if I'm going to parse some simplified English.
But with simplified English, the problem is definitely solvable, someone just needs to put their time/money in that. Once UX is good enough for mathematicians, professors or students, it will lift off and be the Wikipedia for Mathematics.
The space of proofs is enormous. Model checkers and proof assistants will probably become user friendly much sooner than they'll get good enough heuristics to navigate such spaces.
Often happens that after an hard proof there are less t'han 10 People that can understand it. Also happened for Fermat Conjecture proved in 1997, after 5k years! Also with shorter proofs can be tricky. I studied at University a proof of Stoker Theorem by Poincaré that fits in one page, but, trust me that it is really diabolic.
He has also criticised the rest of the community for not studying his work in detail, and says most other mathematicians are "simply not qualified" to issue a definitive statement on the proof unless they start from the very basics of his theory.
Math this advanced can be very hard to follow. There are more incentives to do original work than check someone else's, especially when they have drifted far off the mainstream. It takes a special arrogance to say, "You have to come to me" and then be angry when nobody follows.
> "simply not qualified" to issue a definitive statement on the proof unless they start from the very basics of his theory
How is it arrogant to say people need to study the whole branch, from the beginning, rather than just try to cherry pick a few advanced parts of it, if he really did come up with a substantially new branch?
That sounds more like practicality than arrogance to me.
It is quite a risk to spend a year or more in dedicated study before seeing any results whatsoever interesting. Why are there no basic lemmas in this new theory?
As I recall, he's personally tutoring at least one other mathematician, doing lectures, etc -- that is, I'm pretty sure he's doing the last two of your suggestions. Writing books, of course, is a multi-year process in addition to his other work.
The problem is that they're disqualifying people who study under him in this manner from verifying his work, which seems like something of a catch-22.
It's tough, but that standard exists for a reason. They want it to be somewhat arms length. But this means that if you go too far off the beaten path, it's hard to follow.
I agree that the standard exists for a reason; my point was that it's unfair to characterize him as not trying.
The standard doesn't just make it hard to follow someone who sets out a new branch in depth - it makes it virtually impossible for an extended period of time, because it disqualifies anyone he guides. Such a standard requires that we essentially wait 5+ years (at best) until either high quality maps or guides trained by the initial guided group exist. (And even then, we'll probably wait longer.)
It's not exactly fair to paint that fact as a failing on his part to educate others -- it's a nasty corner case in a generally good academic standard.
In other news, engineers refuse to do a code review of a pull request with 1 million lines of code changed.
As has been mentioned elsewhere, the issue may be the "code bomb" nature of the way the paper was published, and if it was released in even smaller chunks, it may have garnered more analysis.
At the same time one can argue that if len ( Proof1 ) < len ( Proof2 ), where Proof1 and Proof2 are of the same theorem, then Proof1 imposes less cost, and hence is more valuable, since it will be easier to teach, use. etc.
a frequent situation is that the first proof is really long and convoluted. Later, after building up of much of a theory construction blocks around, the proof becomes "simpler" (i.e. simpler combination of well established in that area "blocks") and that is what frequently taught later to students and to "outsiders".
For such first long proofs among the best approaches is to throw it to the pack of hungry wolves ... err ... students and first years PhD-s and let them gnaw on it (with presenting their progress on weekly department seminars - thus saving time to more valuable members of the department and providing the students with real-life experience of a mathematician) Well, at least this is how it was done back then at our University (in Russia :).
He probably should try to use Coq proof assistant. If Coq proves his proof, then mostly like it's correct. Of course, it's easier to say than to do, not a trivial work, and he's the only one who can do it, since he's the only one who can understand the proof.
But if he indeed able to write the entire proof in Coq, then I'm sure at that point, his proof will be much cleaner as well.
That is like a complete no-go. It took something like 6 years[0] to formalize the proof of Feit-Thomson, one of the first "long" proofs in group theory, and that was done by experts who understood both Coq and the proof. In the time it would take him to write the proof in Coq, dozens of mathematicians could learn the theory and independently verify it.
"Oh my god, it's such a big project, nobody should do it alone". It's very obvious, isn't it? 500+ pages of abstract proofs need to be expressed into some kind of programming language. Not to mention, the worst case is that he doesn't even know what coq is, or have never used a programming language (probably just TeX, since he's mathematician) and will take him sometime to pick it up, and then learn how to express his idea using it, etc ...
Look at the linux kernel we have right now, let's go back to early 90s, and should we tell Linus not to do it because it's so big? And did it end up Linus doing it all alone himself?
Coq is certainly not a short term solution, but definitely a valid one if no one else wants to read his proof, and it's very important for him validate it.
The reason I bring Coq up is that in general, I do feel proving things in maths is very much like writing a program in a programming language. Maybe the 500+ pages of proof is like a spaghetti code, refactoring might make it more readable, or more clear, so people are more likely to study it. Or the 500+ pages of proof is very elegantly constructed, just need someone to appreciate it. Coq can certain help in both cases.
But then is it worth it for him to do it? That's really he's judgement call based on how important the proof is, what he see he can get out of this, etc.
Remember that line from the article you quoted: "Fun ~enormous!"
Writing a program is exactly the same thing as proving a mathematical statement. This is an extremely cool and deep result. Start with the Church-Turing thesis and go from there.
Sure. But no dozens of mathematicians are stepping up to take the roughly half a year (and novice-like zen) he anticipates it requiring to understand the proof. So if he wants it to happen: do a lecture series, or programmatize the proof, or write an expanded walkthrough book series to explain it in less condensed form. Or just complain to new scientist and see if any new folks decide to pick up the torch, I guess.
I understand the trouble, but in this case it seems like the trouble might well be worth it. If the ABC conjecture is proven, the consequences are quite substantial:
Guys. This is my problem with reading white papers. People use notations and assumptions which I am not familiar with. Hence, I have to go decipher what people are trying to day. There needs to be a course for math notation. Is there a book or a online course I can take to familiarize myself with math as a language.
They use (slighly) different notions in different parts of mathematics. And usually, it's not just the notation that's difficult, but the concepts themselves.
In general, you are best off studying introductory texts to the topics you are interested. You will pick up the notation.
I have a similar issue with a philosophy that I'm creating.
There are some barriers. Off the top of my head...
1. The reader has to care enough to expend time & energy to understand the concepts
2. The reader comes in with an Existential Context that may have to be suspended or expanded. This is tricky because Existence is a fractal of nuance and it's difficult to know when there's a misunderstanding. Conversations & isolating examples help.
3. The reader has to be willing to adopt the new Existential Context while reading the works.
4. The more ridged & complex the context, the more the reader has to deny self.
I'm kinda amazed that no one has been able to write a proof solving AI yet. While a human AI is a very daunting task in order to capture "humaness" and large problem-set it would seem to me that an AI working solely as a domain expert within maths should be much more feasible.
Shouldn't you be able to build a database of all current proofs and have a computer be able to cross-reference and extrapolate from that? Sure it would be far from trivial but it seems doable. Mathematica/Wolfram for instance should be half way there.
Here's the golden chance for a programmer to win x amount of Nobel prizes! :)
There are computer generated proofs. They are also completely unreadable, much less understandable, by humans. In reality, most of mathematics is based on set theory, which makes it hard for computers to reason about proofs. There is currently an effort to rebase mathematics on type theory, which would allow computers to verify and create proofs much more easily. However, basically all of mathematics has to be reproved using this new foundation. To give an example, group theory as taught in undergraduate classes depends completely on sets. A group itself is a set with additional properties. Subgroups are defined in terms of set intersection and union. Type theory is still in its infancy, and this stuff is still being figured out. In terms of Mathematica, it doesn't know jack shit about complicated math theorems. Can it tell you if a group is solvable?
Yeah, classifying math aspects and creating relations between different proofs is probably one of the thornier issues I'd guess. It does feel however that mathematics is a domain where an AI should be able to train itself in some way
Some time ago I started designing a system that would convert between automated checkers syntax and some simplified human-readable English. But failed, once realized the problem is bigger than me.
Here I just want to encourage anyone who thinks he's a good programmer to develop such a system. It would be extremely useful for education as well: students would get a tool that explains complex proofs, and professors would give assignments to put a theorem into the system (if student is able to enter the theorem into the system, then he/she definitely understands it up to the very foundations). The main problem to solve is good UX, not the math.
They who manage to make the system, the new verified Wikipedia for Math, would have their names inscribed for eternity, because Math is eternal.
yes, that's why I think something different than Automated proof checking for solving advanced theorems, you need to have an AI that can take "creative leaps" and break down proofs down to something humans can understand, and not just verify existing rules
You mean x amount of Fields medals. There is no Nobel for math.
Also, this is a lot harder than you think. "Extrapolating" from a learning set is relatively easy to do for statistical problems and prediction, but proofs are hard.
- An error was found in 2012 and was just recently (Nov 2014) corrected - He's re-released his notes & lectures on the subject - A workshop will be held on the topic in March
That doesn't seem to be unusual / isolationist behavior, though it's obviously a complicated topic and since Fermat's Last Theorem has been deemed 'solved' already, the fact that it makes a FLT proof easier isn't much appreciated by the press / community.