An ABC proof too tough even for mathematicians

Abstract Maths is like having a Organic Chemist working on understanding the transformation of food at the molecular level. A Software Programmer is like a cook who knows how to mix and prepare food in order to make a delicious dish out of it.

It isn't a new algebra, calculus, or geometry. Not to minimize the accomplishment at all, but it happens a handful of times a generation.

So long as the original intuition is actually correct, then any bug will probably be patchable. (Obviously there's no guarantee!)

To stretch analogies:

It seems like you're analogy is saying: My card pyramid is built, but now if I remove a card, it all falls down.

The more apt analogy is: When you're building a structure, you might be off a little the first time you build it, but if the overarching design is sound it will still work out and you can fix it and try to be perfect again. If the overarching design is not sound, you won't be able to build it at all.

What I'm trying to say is, problems in the more bottom layers are very unlikely.

I cannot really give a complete explanation, being unfamiliar with his papers. But to argue by analogy, suppose I had invented a difficult and programming language. How might I persuade you to learn it? One way would be to use it to solve problems that are known to be difficult very easily, elegantly, or extensibly.

It is the same with "inter-universal geometry". One should not have to follow Mochizuki's work all the way through his proof of ABC to know whether it is good for anything. What is the quickest route to a surprise? What can Mochizuki now do with less effort than the existing experts?

The absence of good answers is behind skepticism of the proof.

Take the Fermat-Wiles proof. It's probably the most significant number theory result of the last century, yet it doesn't contain new profound number theory. Its genius is the use of elliptic curves, which is algebraic geometry.

I'm not saying Mochizuki's proof doesn't contain new profound number theory, but this is a very possible outcome, we just don't know yet.

Have you tried thinking up new mathematical objects? What do you tend to come up with? (Not snarky, I'm genuinely interested - maybe some people's creativity works differently to mine)

>Wait, so you're saying it's easier for humans to prove complex theorems than computers?

Of course! If proving theorems could be readily automated, this would have been done already. Indeed, automation has succeeded for some kinds of problems (e.g. google Wilf and Zeilberger's "WZ method" in combinatorics for a particularly successful example)

>Doesn't that mean that verifying proofs is then based on a super handwavy process where a bunch of researchers come to a consensus and say "yes, this is correct"?

Basically, yes.

>What if they all overlook some crucial aspect because of the way they were trained, or their entrenched / ingrained assumptions?

This happens surprisingly rarely. It helps that we are trained to constantly question our entrenched assumptions.

>Could we maybe have a common database of well-known proofs, axioms, concepts etc, so that you wouldn't have to rewrite common ideas from scratch?

Various books fill this purpose. But the problem is that theorems are difficult to encapsulate. For example, a theorem will say "Assume X, Y, and Z. Then A and B are true." and you need to use it in some situation where Z isn't true, but some appropriate variant of Z is, and any expert would know how to conclude that A and B are true. This is when the handwaviness comes in.

Mistakes do happen. But surprisingly rarely.

http://terrytao.wordpress.com/career-advice/there%E2%80%99s-...

Computer proofs tend to be brute force. For example: Are all games of Freecell winnable? But a brute force run of all Freecell games just tells us that all but one game is winnable, but tells us nothing about what's happening or why.

Complicated theorems, like the four-color theorem, are different point. Note there though that the original proof of the four-color theorem, which was based on a computer enumeration, was not convincing to many mathematicians when it first came out, in part because it wasn't feasible to verify manually. Researching now, I see that a proof verified by Coq now exists, which I think reduces the amount of distrust.

Yes, mathematicians "come to a consensus." And they make mistakes. Proofs are sometimes believed to be correct for several decades before being shown to be incorrect, though for important proofs - proofs that others depend on - that's extremely rare. But it isn't super handwavy. They've developed processes over time to help identify flaws. This link outlined a few of them: many people work in the same area, so they can cross-check, and workshops and other meetings serve as a way to spread knowledge and get feedback. Note how it will be a couple of years before the proof is published.

If there's a missing crucial aspect, then that may reveal new types of math. Consider the work of Cantor. Quoting Wikipedia, it was "so counter-intuitive—even shocking—that it encountered resistance from mathematical contemporaries such as Leopold Kronecker and [others], while Ludwig Wittgenstein raised philosophical objections. Some Christian theologians (particularly neo-Scholastics) saw Cantor's work as a challenge to the uniqueness of the absolute infinity in the nature of God ... The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics, and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth.""

Nowadays, Cantor's work is considered the origin for set theory.

Part of the training in math is to make those "semantic things" well-defined.

If you go further into the philosophy involved, then you start dealing with formalism, where everything is reduced to symbols manipulated by a grammar (hence how Stephenson's 'Anathem' refers to computers as 'syntactic devices'), and with Zermelo–Fraenkel set theory, which is one of the most common foundations of mathematics. However, then you have things like the continuum hypothesis and the axiom of choice which are not part of the the ZF set theory, leading to ZFC set theory. And at this point I'm well beyond what I know about the philosophy of mathematics.

Suffice it to say that a full formalist description of a theorem, such that it can be reduced to a machine proof, is hard. Take a look at "Principia Mathematica" by Whitehead and Russell. Among other things, it used logic to show that 1+1=2. (See the end of the proof at http://en.wikipedia.org/wiki/File:Principia_Mathematica_theo... - "The above proposition is occasionally useful.") That might give you a idea of what the effort looks like.

Often times, a proof is (much) more complicated than just mixing theorems A, B, and C together to get result D. Many times proofs will require developing entirely new mathematical structures, or can be done only in steps.

As an example, a friend of mine just proved a great theorem about whether or not Hessenberg varieties can be paved by affines. Ignoring what this actually means, the proof involved firstly recognizing that a Hessenberg variety actually fits within a spectrum - it is somehow "between" other types of well- (or better-) understood varieties. These are paved by affines in (somewhat) obvious ways, and so it is natural to try to use the "between-ness" of the Hessenberg variety to construct a "between-ish" paving. This isn't a proof, but it is a direction (one that turned out to be fruitful). It would be very hard for a computer to have made this intuitive leap.

And it almost works. Except now you can't reduce things like you would like, and you need to construct multi-level fiber bundles in order to get the triviality that you want. And wait - this only works if the Hessenberg variety that we started with has such-and-such property.

So she's reduced the problem to a simpler problem. How does she know it is simpler? Intuition. A computer would have a very hard time recognizing whether or not this is actually simpler (even if it could get there). It turns out that this property holds when our Hessenberg variety is constructed from an element whose semisimple part under the Jordan decomposition is regular. So she has proved it for a huge class of varieties, but not all. Such a partial result would also be very difficult for a computer, since it isn't exactly what she set out to do. She's only partly there. But even this part is huge.

And there isn't anything hand-wavy about her argument, either. It's perfectly grounded in well-established theorems, all of which she understands the proof for. It's just that the original concept was shakey - the "between-ness". She had to work to ground it. It would have been exceptionally hard for a computer to make several of the intuitive leaps necessary to come up with the ideas for the proof in the first place.