Mathematician's anger over his unread 500-page proof | Hacker News Reader

Mathematician's anger over his unread 500-page proof

newscientist.com

126 pointsca98am79114 comments

This and many comments seem to miss the facts, at least as presented on the ABC conjecture's wikipedia page http://en.wikipedia.org/wiki/Abc_conjecture:

- 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.

Hey, it's New Scientist - http://www.wired.com/images_blogs/beyond_the_beyond/2009/07/...

The angry isolated maths geek sells better.

This happened to Scientific American though and I stopped buying it.

On a long enough timeline, it seems all popular science magazines may turn into Focus.

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.

Sure, publish the reduced paper in the journal, then have the "Scenic Guide" in your webpage or ArXiv, or wherever

Or, I dunno, just create a subreddit or a StackOverflow page for it

The best, most readable version is often the author's dissertation, although this obviously only applies for the works of graduate students.

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.

Another reason that paper journals are no longer the ideal medium for scientific research.

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 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.

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 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.

maybe he'll pull a Galois and submit a suitable paper shortly before a pistol duel.

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.

Math is supposed to be about pursuit of truth, not how congenial you are.

Like it or not, but math these days is a kind of social activity.

Come on! Maths is about passing on messages, and this is a human endeavor.

He's welcome to pursue truth on his own, but if he wants other people to read his proof, it's more about the people than the proof.

A message remains true even after encryption, and yet it's unreadable.

But you can only make sense of it if you have the key... Or already know how to crack the code.

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.

I'm not so sure this is entirely his fault.

EDIT: tpyo

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.

Don't feel bad. I can't get coworkers to read 2 page approach docs.

I not too sure about emails with ten lines.

> 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]

[1]: http://en.wikipedia.org/wiki/Classification_of_finite_simple...

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.

First of all you have to prove that a computer program is capable of verifying all unknown theorems correctly. This may be tricky.

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.

But perhaps one can verify all provable theorems.

Could a computer verify that the domino problem is undecidable? The proof consists of translating the problem into non-halting universal turing machines.

http://en.wikipedia.org/wiki/Wang_tile#Domino_problem

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.

A proof, even if true, is worthless if it is unusable by others to build proofs on top of it.

> Grigori Perelman, another mathematician who refused to engage with the mathematical community

That’s not quite it.

http://www.newyorker.com/magazine/2006/08/28/manifold-destin...

That article isn't quite it either: http://en.wikipedia.org/wiki/Manifold_Destiny#Controversy

Hopefully someday, model checkers and proof assistants can help mathematicians to put these monster proofs into format that can be verified with computer.

Yes, assuming that there remain any proofs which the model checkers and proof assistants haven't already discovered!

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.

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.

https://coq.inria.fr/

There is a really good article here :http://projectwordsworth.com/the-paradox-of-the-proof/. That is from May 2013; the situation is basically unchanged since.

https://news.ycombinator.com/item?id=5685166

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.

You probably mean 5C=D years but the logic is the same... :-)

What are C=D years?

C and D are the Roman numerals corresponding to 100 and 500 respectively. Hence, 5C = D.

But, the larger point was that took 500 (5C) rather than 5000 (5K) years to prove Fermat's Last Theorem.

  I =    1
  V =    5
  X =   10
  L =   50
  C =  100
  D =  500
  M = 1000

  => D = 5C or, equivalently, 5C=D

It's more like 8L years ago, though.

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?

This requires years of in-depth study without guideposts.

If it's a brand new field, help people along the way. (Write books, explain the concepts globally, create projects for Phds, etc.)

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.

> This sense of stubbornness, dignity and pride is a part of what gives him the personality necessary to embark on a project like this

It is always interesting to me, as I see it often in the software world, that people expect extraordinary people to behave like ordinary people.

Fuck you (I'm extraordinary)

I feel for the guy.

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 :).

This would be relevant if there was another proof of the ABC conjecture available.

just take len ( Proof2 ) = infinity

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.

Then again, this will never happen.

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.

[0] http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/

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.

"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.

Except in Math we accept duck-typed functions to prove our results. Advanced math is not fully rigorous and often has mistakes.

He will be doing a workshop:

RIMS Joint Research Workshop: On the verification and further development of inter-universal Teichmuller theory (in Japanese) http://www.kurims.kyoto-u.ac.jp/~motizuki/2015-03%20IUTeich%...

March 9-20 2015

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:

http://en.wikipedia.org/wiki/Abc_conjecture#Some_consequence...

On a side note: What is the Latex font name used in this document (Published by Shinichi Mochizuki)?

http://www.kurims.kyoto-u.ac.jp/~motizuki/IUTeich%20Verifica...

Looks really nice to eye.

Computer Modern http://en.wikipedia.org/wiki/Computer_Modern

> If nobody understands a mathematical proof, does it count?

That depends. If it deals with integers, yes. If it deals with real numbers, no.

boo. hiss. (and actually a clever reply tottenhm)

s/anger/frustration/

"An overview of Inter-universal Teichmüller Theory and [...] how we can begin to understand this theory":

http://www.quora.com/Joseph-Heavner/Posts/An-overview-of-Int...

Also, from an anonymous post on 4chan @ http://boards.4chan.org/sci/thread/6931488/are-you-ready-for... :

"How to understand IUTeich from the bottom up:

- Algebra (Israel Gelfand)

- The Method of Coordinates (Israel Gelfand)

- How to Prove It: A Structured Approach (Daniel Velleman)

- Kiselev's Geometry - Planimetry and Stereometry

- Trigonometry (Israel Gelfand)

- What Is Mathematics? An Elementary Approach to Ideas and Methods (Richard Courant)

- A Course of Pure Mathematics (G.H. Hardy)

- Linear Algebra (Kenneth Hoffman and Ray Kunze)

- Elementary Differential Equations (William Boyce and Richard DiPrima)

- Topology (James Munkres)

- Calculus On Manifolds (Michael Spivak)

- Principles of Mathematical Analysis (Walter Rudin)

- Real and Complex Analysis (Walter Rudin)

- Functional Analysis (Walter Rudin)

- Partial Differential Equations (Lawrence Evans)

- Analysis On Manifolds (James Munkres)

- Abstract Algebra (David Dummit and Richard Foote)

- Algebraic Topology (Allen Hatcher)

- Introduction to Smooth Manifolds (John Lee)

- Foundations of Differentiable Manifolds and Lie Groups - (Frank Warner)

- Galois Theory (Harold Edwards)

- Linear Representations of Finite Groups (Jean-Pierre Serre and Leonhard Scott)

- A Classical Introduction to Modern Number Theory (Kenneth Ireland and Michael Rosen)

- Introduction to Analytic Number Theory (Tom Apostol)

- Modular Functions and Dirichlet Series in Number Theory (Tom Apostol)

- Riemannian geometry (Peter Petersen)

- The Theory of the Riemann Zeta-Function (Edward Charles Titchmarsh)

- An Introduction to Teichmüller Spaces (Yoichi Imayoshi and Masahiko Taniguchi)

- A Course in p-adic Analysis (Alain Robert)

- Foundations of p-Adic Teichmuller Theory (Shinichi Mochizuki)

- Mochizuki's papers at http://www.kurims.kyoto-u.ac.jp/~motizuki/papers-english.htm... "

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.

This man invented bitcoin.

I thought he looked familiar... I definitely remember his photo making the rounds as "Potential Satoshi"'s when that was the media craze of the week

yup, i recognized the photo as well http://chartgirl.com/wordpress/wp-content/uploads/2013/05/SA...

Do you people not understand most of that infographic is a joke?

What real-world purpose does this conjecture hold, and why is its proof of any importance?

see

http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem

http://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Monetar...

? The Fermat prize money has already been collected. If the real world purpose of this conjecture is to collect prize money, it won't be that prize.

Andrew Wiles already solved that...

http://ars.userfriendly.org/cartoons/?id=20070105

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! :)

This is an area of research: http://en.wikipedia.org/wiki/Automated_theorem_proving

Automated proof checking software has been around for a while, and they don't really require any capacity I'd describe as 'AI' as they simply verify logic: https://en.wikipedia.org/wiki/Automated_proof_checking

The trouble is that writing a proof in a format amenable to this verification is harder and much more tedious than writing it for a paper

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

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.

https://en.wikipedia.org/wiki/Automated_theorem_proving

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.

Ah sorry that's right, I always forget, maybe one in Economics then :)

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

Why are types easier than sets? They are both computable.

Reply on news.ycombinator.com