Hacker News new | past | comments | ask | show | jobs | submit login
An ABC proof too tough even for mathematicians (bostonglobe.com)
282 points by ot on Nov 25, 2012 | hide | past | web | favorite | 142 comments

The more mathematically-inclined HNers might be interested in Brian Conrad and Terrence Tao's comments at the bottom of this previous HN article:


Edit: Minhyong Kim's initial thoughts seem very interesting as well!


And for the less mathematically-inclined:


If a programmer locked himself away for 14 years and then emerged and announced he'd written a completely bug free OS, there would be skepticism. Code needs to be battle tested by other people to find the bugs.

Mathematics is the same, to an extent; one guy working alone for 14 years is likely to have missed ideas and perspectives that could illuminate flaws in his reasoning. Maths bugs. If he's produced hundreds of pages of complex reasoning, on his own, however smart he is I'd say there's a high chance he's missed something.

Humans need to collaborate in areas of high complexity. With a single brain, there's too high a chance of bias hiding the problems.

It is worth noting that Andrew Wiles' initial proof of Fermat's Last Theorem also had a bug. This was later fixed, with help.

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

However, it soon became apparent that Wiles's initial proof was incorrect. A critical portion of the proof contained an error in a bound on the order of a particular group. The error was caught by several mathematicians refereeing Wiles's manuscript.[112] including Katz, who alerted Wiles on 23 August 1993.[113]

Wiles and his former student Richard Taylor spent almost a year trying to repair the proof, without success.[114] On 19 September 1994, Wiles had a flash of insight...

I do not think it is fair to compare Software and Abstract Mathematics. Software is mostly an Engineering problem, while Mathematics is mostly Science and Conjecture.

And even if they locked themselves for 14 years, there is no "single mind at work" there. Mathematics are built "on the shoulder of giants" through generations of brain dedicated to it. There is no such thing as pure invention - new discoveries lead to new theorems, new leads that other people take on.

I agree that Mathematics is usually built "on the shoulder of giants", but the gist of that whole Wired article is that this dude has created a whole new branch of maths, on his own, to prove this theorem. Sounds brilliant, but risky.

It's a branch as mathematicians think of branches, not as laymen do.

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.

Let me say it in another way.

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.

This is not a good analogy. Many programmers have training in computability theory and understand some very discrete principles. Just because they may become entrenched in UX or some other facet of coding, does not mean they're just "hacking" stuff together in a pleasing way.

"A Software Programmer is like a cook who has an undergraduate degree in Organic Chemistry." May be a more apt analogy.

"Programming is one of the most difficult branches of applied mathematics; the poorer mathematicians had better remain pure mathematicians."– E. W. Dijkstra

Dijkstra did a kind of programming distant from most of it today. If to him programming is a difficult branch of applied mathematics, then HN is a forum talking about how best to calculate your tip after dinner.

You guys really are masters of specious analogies. Comparing the best of one field to the worst of another isn't a legitimate comparison and you know it.

Both are difficult, but at least in programming you can rely on manipulating actual "elements" of information. There is some tangible part in it, while sometimes very remote in certain cases. Abstract Mathematics go into spaces of n dimensions and stuff that most programmers would not be able to comprehend, just like most human beings cannot without tremedous time and effort.

I think it is a false debate to say that one discipline is poorer or more valuable than the other. We need both Mathematicians to advance the theories and Programmers to apply their learnings into the real world. Everyone has its place.

I agree with the thrust of what you're saying (one discipline is not poorer or more valuable than the other) but I take exception to your "campus supremacist" tone. True, organic chemistry and cooking serve different needs, but the organic chemist can appreciate cooking while the cook cannot appreciate organic chemistry, and the same superset implication is present in your second analogy (that programmers cannot appreciate N-dimensional spaces).

I'd be more worried about this attitude if I thought you had much comprehension of the overlap of these fields. To take your own example, many machine learning algorithms begin with N-dimensional spaces (you know, the kind programmers can't comprehend) and go from there—support vector machines are the obvious example ("a support vector machine constructs a hyperplane or set of hyperplanes in a high- or infinite-dimensional space"). But that's just the beginning; the Curry-Howard isomorphism shows that proofs and programs are the same thing. That theorem provers exist at all seems to undermine your original point. The category-extras package for Haskell, which is a set of abstract algebraic entities that, to my knowledge, are used exclusively for mathematical experimentation and not of any practical application at all.

On the other side of the coin, the only practical applications of number theory have been in cryptography, and the big name there (RSA) is simply modular arithmetic combined with things we expect to be true about large primes. This level of math produces practically applicable results roughly every thirty to fifty years. It's wonderful when it happens, but the idea that mathematicians are consistently churning out theories of practical import is laughable. We do have people doing that, and we call them applied mathematicians and computer scientists.

Are most programmers sufficiently mathematical? No—Dijkstra bemoaned this at great length. Does this mean that mathematicians are somehow a superset of programmers? Absolutely not.

Let me be clear. I'm arguing with your tone and the implication behind your ham-handed analogies. What you've simply stated (we need both), I agree with.

The Curry-Howard isomorphism doesn't explain away mathematics. There are next to zero large and important theories of mathematics which have been formalized in a computer language. It's partly due to the difficulty of proof automation---the solvers are very young---but mostly because proofs are just the pickaxes for mathematics. Right now human-driven proofs are far more powerful tools.

Programming benefits greatly from a tiny section of mathematics and the more deeply the connection between the fields grows the more we'll see strong justification for universal patterns in programming and strong realization of abstract mathematics.

It's also a bit of a strawman to pick just number theory as the only field of mathematics to examine for practicality. Our world as we know it today would not exist without diffeq and your own example of machine learning really is just applications of optimization, statistics, probability, and abstract geometry.

"We need them both" is an unrefined statement. They are apples and oranges, though a mathematical programmer might be uniquely powerful as might a programming mathematician (Djikstra?).

I'm absolutely not trying to explain away mathematics. I'm just not letting a "mathematics is superior to computer science" perspective slide in under the carpet, and I'm marshaling a variety of areas of overlap to illustrate that there is not a strict superset relationship between the two fields.

I chose number theory specifically because that's the subject of the ABC conjecture whose proof spawned this whole debate.

Mr Dijkstra obviously did not code in Ruby.

I'm confident he'd look on Ruby as an insult.

I am confident people might believe something they don't understand to be an insult..

I don't follow you.

I was hinting ignorance might be the cause of your confident dismissal of Ruby :)

@btilly: it seems as though that would be a correct assertion.

@jacques_chester: I did not know that, does he have a piece on programming languages he found disconcerting? Did he prefer Church over Turing?

I don't think programming languages can really go beyond being strictly mathematical though..

Ruby is probably the language I've written more code in than anything else. I quite like it; I find myself chafing in lots of other languages.

My point is that Dijkstra was kinda big on programming-as-strict-mathematics; a loosey-goosey super flexible language like Ruby would not have met with his favour, IMO.

I think that ignorance of Dijkstra may be the cause of your confident appraisal that he would have liked Ruby.

His wikiquotes page will give you a flavour of his thought:


But especially "On the Cruelty of Really Teaching Computer Science".


In theory - The reality is there is not a working compiler except for a few special cases.

Not quite. Proofs, in practice, are not programs. They do not contain every detail, nor are they written in completely consistent language.

I don't think he's claiming "bug free" -- and if I remember right, people have already found "bugs" and he claims to have a patch that he'll post soon. There's a huge difference between minor errors that invalidate the proof but can be fixed easily once they're noticed and fundamental errors where the proof is just wrong and can't be fixed. So most of the bugs that you're talking about don't really matter (of course, "bugs" that seem trivial at first might turn out to be fundamental irreparable errors, but that's a separate issue).

But a mathematical proof is like a card-pyramid, building steps upon steps to reach a very specific peak. Any bugs anywhere in the structure could be serious indeed, unless they can be patched.

This is kind of true, but not quite right. If there's a flaw serious enough to be too hard to patch, it's likely that some problem would have come up later. That is, some serious contradiction would be reached, or something really weird would happen that yells "either this is really unexpected, or you have a problem earlier."

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.

Hmm, yes I can see your point. The internal consistency of maths would be quite a good debugging tool.

Sure, but each step was probably reached with the aid of intuition -- in other words, the mathematician suspected that it had to be true before they found the particular formal proof employed.

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

I think it's more like if a programmer locked himself away for 14 years and then announced he'd written an OS before anyone else. Even if the whole thing is riddled with bugs (and let's not forget this programmer is more on the Bernstein end of things, precision and confidence are high) it's still some place potentially worth exploring.

But nobody would quite yet. Instead he announces one more thing, he's used this OS to control a rocket ship and send a satellite to Mars far before anyone else has even come close!

Now, assuming he didn't lie there, you really want to figure out what he invented because he just seems to be vastly more powerful than you.

Agreed but I think there is value in independently-evolving ideas.

From my own experience; the more I am connected, the more I share and optimize existing ideas. If left on my own, I will come up with rough but more original ones.

A 64 bit operating system built over 7 years from a guy here on HN called losethos: http://www.youtube.com/watch?v=WAr-xYtBFbY

Tragically, the author suffers from a severe mental illness and has been banned from HN, Reddit and others.

Even if his proof turns out to be flawed, It is likely that the new system he constructed will still provide us a new and usefull way at looking at math. The good thing about working outside of mainstream is that their is far less inertia holding to the old ways. Assuming his work does represent a new branch of math, he has reduced the problem of the rest of us discovering/inventing it from stumbling blindly to making sense of his papers.

Isaac Newton went away for two years, by himself, to invent Calculus and modern physics.

Gottfried Leibniz "invented" calculus around the same time as Newton. Indeed, the dy/dx notations were Leibniz's.

Wolfram wrote ANKOS in the way you describe.

And ANKOS has been criticised for not being rigorous enough.

As a counter example: Time Cube guy came up with Time Cube in the way I describe.

Another article with slightly more background on the ABC problem itself (and possibly slightly less sensationalist). http://www.nature.com/news/proof-claimed-for-deep-connection...

And the MathOverflow discussion referenced: http://mathoverflow.net/questions/106560/what-is-the-underly...

I think implying the article is sensationalist is a little harsh. It's definitely a click-grabbing headline, but overall a decent article on a tough subject.

Seemed extremely hand-wavey to me, and the obscure pictures of 3D wireframe 'A', 'B' and 'C' by the side certainly didn't help.

It tried to explain both the dynamics in math research and the problem at hand, and in the end explained neither.

It's the Boston Globe, hand-wavey is all they can really be expected to publish regarding hard abstract math. I thought they did a decent enough job for a newspaper.

Agreed, I was very please to see a mainstream journal take the time to describe a potentially groundbreaking mathematical discovery

Just read his Wikipedia entry:

> Mochizuki attended Phillips Exeter Academy and graduated in 2 years. He entered Princeton University as an undergraduate at age 16 and received a Ph.D. under the supervision of Gerd Faltings at age 23.

He is 43 Years old now, I assume he is 100% committed to Mathematics. These people fascinate me, having a feedback loop that is unbreakable. Especially for topics where you have a knowledge of something and almost nobody else is the world is capable of understanding you. It's like Star Trek for the mind.

This article seems to suggets that mathematicians are all too eager to drop his work at the slightest whiff of any flaw. Could someone more knowledgable on the subject explain to me why this is?

It is clear that he has already done some very great things in mathematics, so even if there was a flaw in his proof, I would think his papers would still have many deep insights that no else had thought of. I mean, it's not like mathematicians are pressed for time -- if I was one I would certainly dedicate a lot of time to studying something interesting like this.

You clearly do not value the time of mathematicians like they value their own time.

The estimate that I was told for the average mathematician reading the average math proof is one page per day.

Thus the average mathematician facing this will see 750 pages just to becomes of the the 50 people who have mastered the basics of anabelian geometry. That's 2 years. Then you have to take on some unknown number of years to learn "inter-universal geometry". Then your reward for doing this is that you are qualified to read a 512 page proof, which is again going to be a year and a half. Along the way if you find a mistake in any of it, your reward is to confirm the immediate guess that most mathematicians have which is that there is likely a mistake somewhere. (But with this much math, you'll probably find several "mistakes" that aren't before you find a real one.)

This is years of work, that has nothing to do with anything that you're already working on. And believe me, a professional mathematician has no shortage of problems to work on, in areas that they already have the background for.

If you think that this is unreasonable, well, why don't you volunteer to fix it? Reading the proof shouldn't take you much longer than it would take to become a mathematician. And you can learn anabelian geometry during grad school, so that time is not all wasted.

>> The estimate that I was told for the average mathematician reading the average math proof is one page per day. Thus the average mathematician facing this will see 750 pages just to becomes of the the 50 people who have mastered the basics of anabelian geometry. That's 2 years.

Ah, well I did not know this. I appreciate the enlightenment. I see the trepidation of reading the whole thing then.

Even more importantly, you might take all that time to review it and the miss a mistake that's actually there, thus wasting all of your time (for some definition of waste).

Right now we are waiting for his corrected paper, as the current one contradicts some known number theoretic results. Mochizuki put uP an amazing amount of scaffolding and invented a new area with new abstractions. People who I trust claim that there isn't new profound number theory in this, so then it may become a matter of whether to study an learn it for its own sake, which carries less incentive if there is no immediate application.

Plus: mathematicians really don't have spare time to learn every area that comes along. Allegedly Poincare was the last true polymath. Given how math has been developing for centuries and you never really need to throw things away it continually becomes harder to get up to speed in any particular field. There's a famous quote about how the Princeton undergraduate math program is so rigorous that it brings you up to speed, to the point of early twentieth century mathematics. In this way math is incomparable to CS.

"there isn't new profound number theory in this"

I find this claim very surprising.Saying that "there is no new profound number theory" implies a deep understanding of the totality of Mochizuki's work, which as far as I know is so complex and far from the current state of the art that nobody really understands it yet.

Mochizuki's work may prove to be right, and it may prove to be wrong. But saying there is no new profound number theory at this point seems a little premature.

+1, you ask a very important question, which I can at least sort of answer. I think it's key to understanding why many experts think Mochizuki's work is likely to be wrong.

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.

As an outsider all this (line of reasoning--not personal) just sounds like is "not invented here" syndrome. That may or may not be fair. But isn't this what tenure is for? You can't get fired for just learning, right? Why is there so much lack of intellectual curiosity and so much self-centered-ness on "academic ambition". Are the two so self-contradictory? How much great work has gotten swept up under the rug by this attitude toward "peer review"?

I am not sure I understand all of your questions, but I assure you that if people believed there was a high chance that the proof was correct, then they would be very eager to read it.

Mathematicians, and especially the very best mathematicians, are very eager to learn. I don't know of any great mathematician who demonstrates a "lack of intellectual curiosity".

That said, there is much more mathematics available than anyone has time to read. It can easily take an hour a page, or more, to read a dense research paper. Mathematicians, like everyone else, have to be selective about what they choose to learn.

It is very rare for great work to be ignored, but here is one example:


Perhaps is it not so premature, since this proof relies mainly of this new inter-universal geometry,

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.

Nice to know, thanks!

Seems quite the opposite. The article says most mathematicians have well-established lines of research and are disinclined to devote years to understanding a different specialization. The mathematicians who are trying to understand the proof are described as young, up-and-coming mathematicians with little to lose and a lot to prove (and an opportunity to potentially get in on the ground floor of a new theoretical framework -- "inter-universal geometry")

Mathematics - at least some kinds of it - is largely a game of symbols. You define something and then see if you can prove anything about it. Most of the time, it turns out to reduce to group theory (e.g. Galois theory basically consists of reducing the study of fields to the study of groups). Sometimes you come up with a novel structure about which you can say something. Occasionally, this gives you a result that feeds back into another branch of mathematics, or even into number theory - as with Wiles' proof of Fermat's Last Theorem. But most of the time, this is just some funny structure and you say "well, that's nice" and move on.

So Mochizuki has almost certainly defined some new objects and proven some things about them. But mathematicians do that all the time (admittedly on a smaller scale). If you just want to look at something, there's plenty of "new territory" around - stuff that doesn't require learning a new notation, and hasn't had Mochizuki looking at it for ten years already. The only reason some arbitrary new structure is interesting enough to spend your time learning about is if you can tie it back to number theory.

> Most of the time, it turns out to reduce to group theory

I'd be really interested if you could justify this! Sure, group theory has a huge number of applications across mathematics, but to say that it reduces to group theory "most of the time" seems completely implausible.

What I mean is: if you try, starting from nothing, to make up the definition of some new kind of object, and then start proving things about it, most of the time you find that you've defined a group or something that reduces to a group. I don't have a quantitative measure of this (I can't really define a probability distribution for "random objects you think up"), it's just personal experience. Put another way: I find it quite hard to think up a new object that doesn't turn out to just be a group.

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)

> Have you tried thinking up new mathematical objects?

Yes, I have. Off the top of my head, the objects I'm interested in are often monoidal, but usually lack inverses.

Strings don't have any natural group structure (though as free monoids there is an obvious way to extend them into free groups), nor metric spaces or context-free grammars or finite state machines.

Of course groups are ubiquitous, but I think your claims of universality are vastly exaggerated.

funny. yesterday i was trying to explain to my friend, a physics grad student like myself, why i wanted to study algebraic geometry. i said, it's because physicists only know about groups, because everything seems to be groups. but rings have more structure than groups and fields have more structure than rings and that's what algebraic geometry is about. this comment is probably too late. you are right that most things turn out to be a group, but not "just a group".

That wasn't the takeaway I got from the article at all -- and the original proof of Fermat's Theorem by Wiles had flaws that took some work to patch over, but in no way diminished his accomplishment.

I think you've just misinterpreted some of the language used.

"Mochizuki has almost certainly made significant discoveries—but without the allure of a proof, it’s possible no one will take the time to understand them."

"if Mochizuki is able to build up sufficient trust with his peers"

"if an error is found early in the vetting process, the math world will likely move on without bothering to explore the rest of the mathematical universe Mochizuki has created"

I was basing my post on these quotes.

I guess the reason those didn't stick in my mind is that (I think?) they were all interjected by the author -- all the quotes from actual mathematicians said otherwise.

Consider the incentives involved in studying his work carefully for years, and those of being in academia.

I don't think it's even just the incentives of academia, but of life/interest as well. Tenured professors could choose to devote their next few years to learning inter-universal geometry. But they have to guess: is this likely to be a more interesting/useful thing to learn than something else they could learn in those same years? It seems so far that most are heuristically guessing no.

I do not think that is the case. Their is the skeptism resulting from the huge amount of work between accepted math and his results that give mathmaticians concern. It is almost definite that his work contains some flaws, what is not definite is wheather it contains fatal flaws. Many are not willing to invest the time to learn something that might turn out to be useless.

Some relevant background > http://news.ycombinator.com/item?id=4781825

Is this situation similar to that of Louis de Branges & the Riemann Hypothesis a few years back? I.e, a well-respected mathematician (de Branges had settled the Bieberbach conjecture in the 80s) releases a proof of an important unsolved problem using his own poorly understood mathematical technology?

Edit - lest this sound too negative, one should realize that the Bieberbach proof took a long time to be accepted.

A Youtube video with a pretty accessible explanation. http://www.youtube.com/watch?v=RkBl7WKzzRw

Would it be possible to use proof assistants like Coq [1] to verify this kind of proofs ? If not, does anyone know why ?

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

Proofs at this level are nowhere near formal enough for existing mechanical tools to understand. I've seen researchers cite "translated proof X into an automatically-verifiable form" as a major achievement -- even for very simple proofs.

Non-math person here. Wait, so you're saying it's easier for humans to prove complex theorems than computers? That's nuts.

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"? Ugh!

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

When you describe a proof with words like you say, aren't there quibbles over semantic things? But I thought the whole point of a proof was that you leave nothing to semantics. Everything logically follows from each other.

I thought the main issue with proofs systems was that encoding the concepts into code was tedious. 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? Like a package manager with proof-libraries?

Or is this an issue with the expression power of proofs languages?

Yes, it's much easier for humans to prove complex theorems than computers. Just as it is much easier for humans to build complex programs than computers.

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.

I assume that he was going for something different, though; namely, that it's nuts that verifying proofs is simpler for humans than it is for machines.

Well, if the proof is first formalized, it's easier for machines to verify. But formalizing it is much harder. This is similar to the situation in software, where uptake of formal-verification tools that can prove correctness of programs is relatively low (though Agda is making some very interesting progress).

Math person here.

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

Let me add to this. When you try to formalize a proof in a proof assistant, then almost all of the time, you will find numerous errors in the proof.

But - and this is key - these errors are usually fixable or the area is not understood well enough and requires more attention to detail. The human intuition is quite powerful.

That's similar to when you subject working software system to new batch of tests or test it in some new way.

Usually a lot of previously known errors will crop up despite that the system already works mostly as intended.

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

It also helps that finding a counterexample to a widely accepted proof tends to enhance one's career and reputation.

> Of course! If proving theorems could be readily automated, this would have been done already.

It doesn't need to create the proof, just validate it. See P vs NP.

To have an automated proof checker validate a proof, someone would have to lay out every single step in the proof in enough detail for the verifier to do its work. With current verifiers, that means 'in painstaking detail'. Only highly educated and motivated people can do that, it takes ages, and it is not very rewarding (neither financially nor otherwise). Because of that, volunteers are hard found.

In some sense we won't really know whether a proof is rock-solid until we have run it through a verifier, using a proven-correct verifier on proven-correct hardware.

If theorem provers grow to be more easy to use, we may require proofs to be verified, but we aren't there yet by a wide stretch.

For an idea about how hard this can be, check out http://www.cs.ru.nl/~freek/comparison/comparison.pdf: 

"In 1998, Tom Hales proved the Kepler Conjecture […] with a proof that is in the same category as the Four Color Theorem proof in that it relies on a large amount of computer computation. For this reason the referees of the Annals of Mathematics, where he submitted this proof, did not feel that they could check his work. And then he decided to formalize his proof to force them to admit that it was correct. He calculated that this formalization effort would take around twenty man-years"

(that effort is ongoing at http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet)

So would it be fair to say then, that these proof checkers are missing the 'libraries' that would be needed to efficiently write verifiable proofs for modern mathematics?

Exactly. And this is where most of the work on proof checkers is happening -- finding ways that people can input proofs in a less formal way and have automated code fill in the formal details as a first pass before running the verification.

Indeed! This is exactly what I was trying to say!

Right, this was what I was going for. I can't imagine computers being imaginative enough for coming up with proofs, but verifying seems like it should be rather trivial since mathematical notation is already almost rigorous enough to be a programming language.

The more advanced the math gets, the more deeply ambiguous the notation gets. Everything becomes Tx, while T and x become ever more complex objects, whose definiton is implied by context.

Zeilberger has some nice examples of human error on his blog. He would love to see much more use of computer provers to clean up the errors made by human writers and readers.

It's absolutely easier for humans to prove complex theorems than it is to encode it on a computer. Consider if your computer proof system only knows about finite numbers, when your proof deals with transfinite numbers. (There is a one-to-one mapping from each integer to each rational fraction, but there no such mapping exists from the integers to the reals, showing that size of the set of reals is fundamentally larger than the size of the set of integers, despite both being "infinite" in size. -- there is more than one type of infinity.) How do you encode that information

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.

I have to strongly disagree with your first paragraph. Proofs by humans are finite objects, even if they speak about properties of infinite sets. This difference does not make proofs for computers more difficult than for humans. You can encode cardinality theorems easily in interactive theorem provers.

Formally, a proof is a sequence of assertions, where each one is an axiom or follows from previous ones. Humans are better at proofs because they have good and well-developed intuition; it's bit like coding in assembly vs coding in a high level language. The fact that you deal with infinite objects is not relevant.

I was trying to come up with a example where a theorem prover would have to be extended or rewritten in order to handle new types of mathematics. My imaginary scenario is a theorem validator built by mathematicians from pre-Cantor days, where I conjecture that it would be hard to encode transfinite proofs. As I know nothing about how theorem provers work, this is purely conjectural.

In more concrete terms .. and I am so far outside my knowledge that I barely know what I am saying ... I read in the Coq FAQ that "The axiom of unique choice together with classical logic (e.g. excluded-middle) are inconsistent in the variant of the Calculus of Inductive Constructions where Set is impredicative. As a consequence, the functional form of the axiom of choice and excluded-middle, or any form of the axiom of choice together with predicate extensionality are inconsistent in the Set-impredicative version of the Calculus of Inductive Constructions."

In other words, proofs involving "axiom of unique choice together with classical logic" cannot be expressed in at least Coq. While it might be possible to use a machine to check tools which assume the axiom of unique choice, it would no doubt take a lot of work if one needs to build such a system from scratch.

And that is the scenario - where it's much more difficult to develop a mechanical tool than to come up with a proof that enough for humans - that I am contemplating.

What do you mean by "transfinite proofs"? Let's look at Cantor's proof. It is:

For every set A and function f : A -> P(A) there exists y in P(A) such that for all x, f(x) /= y.

Proof: Define y = {a: a is not in f(a)}. If f(x) = y, then f(x) = {a: a is not in f(a)}, but this implies x is in f(x) <=> x is not in f(x), contradiction.

It does not mention infinity anywhere! It only says that there cannot be a surjection between one set and the other. We could call this situation "transfinite" but this is only a name; under the hood, this is a normal proof of properties of functions, using very natural reasoning rules. That's why I disagreed - there's nothing special in Cantor's proof from a formal viewpoint, possible concerns are of psychological/historical nature, which are not relevant to a machine.

It is true that changing foundations might require rewriting the prover. However, humans also need time to adjust to a new formal system. For example, it takes a lot of effort to get a good grasp of intuitionistic logic. This might be a concern, but ZFC is a very well-grounded common framework for mathematicians, and this is extremely unlikely to change. Perhaps calculus of constructions, as a version of lambda calculus, is closer to computation, and this is why it was chosen in Coq. I'm not sure. Mizar (another theorem-proving environment) is based on an extension of ZFC. [ZFC is untyped - everything is a set, while CoC has a rich type system.]

Small nitpick: It's not like proofs involving unique choice + excluded middle cannot be expressed in Coq; they can, but as the system is inconsistent, they have no value, as everything is provable.

This is related to the issue that the criteria for what constitutes a rigorous proof continually evolves, and has undergone tremendous change since Euclid. Morris Kline has a good semi-popular account of this history [http://www.amazon.com/Mathematics-Loss-Certainty-Galaxy-Book...].

I suspect that Godels incompleteness theorems may imply that no single algorithm can solve all proofs. This is actually the basis for Penrose's argument that the mind is non-deterministic, though his argument is deeply flawed.

Penrose's argument, if I remember correctly, is not that the mind is necessarily non-deterministic, but that it is not equivalent to an algorithm - that you can never program a computer to create a mind. It might also be non-deterministic, but that is not exactly the same thing. His evidence for this is indeed that we can "know" the truth of theorems whose proof can not be reduced to an algorithm.

Wouldn't finite, deterministic systems necessarily be able to be modeled by an algorithm? Either the human mind is infinite in some way, non-deterministic, or it must be able to be modeled by an algorithm.

NB I am a programmer and very weak in theory.

There is no algorithm that can determine the truth of any proposition in arithmetic (for example). It is impossible, in principle, to construct such an algorithm. But given any proposition in arithmetic, the mind can decide its truth value. It is in this sense that Penrose claims the mind can not be modeled by a computer program. It may seem odd now, but at the time there was still a school of artificial intelligence that assumed that a big computer running a really sophisticated program could be equivalent to a human mind. Penrose was trying to show that this idea is a non-starter.

    at the time there was still a school of artificial 
    intelligence that assumed that a big computer running a
    really sophisticated program could be equivalent to a
    human mind
We're talking theory, so imagine we have extremely powerful hardware, gobs of memory, understand the brain really well, and have some sort of extremely high-resolution scanning device. We could build an "emulator" that would simulate the brain's "hardware" and then load a scan of someone's brain onto it as "software". The system as a whole is just a big computer running a sophisticated program but it's equivalent to a human mind. This mind running on a computer would have the same strengths and weaknesses as the mind had when running on a biological brain when it comes to determining the truth values of propositions in arithmetic (and everywhere else).

To say that a computer program can not, in principle, do what the mind does is not to say that the mind can not exist on a substrate other than the familiar biological one. In your thought experiment the "software" would not be a computer program as we understand it; it would not be a set of algorithms. Also, it is problematic to separate "hardware" and "software", and to define what a "scan" of the brain might be.

>There is no algorithm that can determine the truth of any proposition in arithmetic (for example).

Currently, yes. But I don't see that this is necessarily true. Why do you think it is?

Simply because there are some propositions that are unprovable in a consistent system with finite axioms. Having an algorithm that solves any proposition would be equivalent to having an algorithm that solves the halting problem.

>There is no algorithm that can determine the truth of any proposition in arithmetic (for example). It is impossible, in principle, to construct such an algorithm. But given any proposition in arithmetic, the mind can decide its truth value.

These two statements seem to contradict, unless you grant that the mind either fudges the proof or constructs new axioms such that the proof can be valid. Why do you assume a program can never do this?

Because the program that does it would itself be an algorithm with its own finite set of axioms. There would be undecidable propositions unreachable by the program.

Solving the halting problem wouldn't be sufficient to tell you whether a proposition was true, but it could tell you whether a proposition is independent and if it wasn't whether it was true or false.

"Given any proposition in arithmetic, the mind can decide its truth value."

Really? I don't see what reason we have to believe that this is true.

I guess I didn't really mean that. What I should have said was that in any system of axioms (or within any algorithmic structure) there will exist undecidable propositions (unreachable by the algorithm). The mind can determine the truth value of some of these, so the mind can not be encompassed or modeled by an algorithm.

> The mind can determine the truth value of some of these, so the mind can not be encompassed or modeled by an algorithm.

Do you have an example of this? I have an extremely difficult time comprehending it. Also, I was under the impression that there weren't necessarily propositions that are not algorithmically possible to reach, but rather, there are always propositions a given algorithm cannot solve.

> not algorithmically possible to reach

I just meant undecidable propositions.

> Do you have an example

Maybe check out the conclusion on p.76 of this book[1] by Penrose (and the argument supporting it that begins on p.72.): "Human mathematicians are not using a knowably sound algorithm in order to ascertain mathematical truth".

His example is our knowledge that a certain computation will not halt, and the impossibility of constructing an algorithm that can prove that fact.

More flippantly, you know that you can examine the soundness of your own reasoning, but no algorithm can reach conclusions about its own correctness.


Okay, so is the twin prime constant transcendental?


Gödel's theorems are about uncountable infinities of statements, and statements whose meaning proof is outside the bounds of a theory. Nothing contradicts the possibility of an algorithm as good as as any human doing formal math.

Terence Tao, one of the preeminent mathematicians working today, had a pretty good post on this exact question:


Good read. You could change a few phrases and make it a post about learning programming rather than mathematics.

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

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.

That's not true for proofs in assistants like Coq, which work by generating a program whose type can be checked to verify the statement in question.

Computers may not be able to solve proofs, but they can help. In fact, there is a BOINC project aimed at finding triples for the ABC conjecture: http://en.wikipedia.org/wiki/ABC@home

Honestly, you sound more like a "non-science" person there. Did you think many branches of science have an epistemology founded on automatic computation? Think again!

This seems overly pessimistic. I'm sure it'd take a lot of work, but consider results like Gonthier's proof of the Odd Order Theorem (see http://research.microsoft.com/en-us/news/features/gonthierpr...), which formalized a book-length proof.

Another famous theorem which is being formalized with a proof assistant is the Kepler Conjecture. It's less than half the size of the ABC Conjecture, with 250 pages of much more elementary mathematics, but the leader estimates it will take 20 years to complete.


...the proof itself is written in an entirely different branch of mathematics called “inter-universal geometry” that Mochizuki—who refers to himself as an “inter-universal Geometer”—invented and of which, at least so far, he is the sole practitioner.

In this universe, at least...

Wouldn't the easiest way to check this proof be to enter it into something like Coq? That way you'd only have to understand how to translate each step rather than learn each field.

You would still have to write 100 pages of Coq code, and write every definition properly, which may be just as hard as learning the field.

"Release early release often" applies to Math as well. Wouldn't it be better for everyone if he hadn't been so secluded and published some of his work in the meantime?

My impression was that he had published some material on IUT before, but nobody had any reason to read it.

I'm a physics student. Sometimes I'm thinking if I should completely change my path to math. I always sucked at it but it seems to be so huge, exciting and powerful.

Can anyone explain what "inter-universal geometry" is?

Different universes in mathematics play by different rules and have different components. Inter-universal Geometry is how these sets of rules and components can relate and is the bridge to understanding more complex theory.


Will the solution(s) to ABC proof be a nightmare to all security protocols relying on prime number factorization, such as RSA?

Whether ABC (or a similar conjecture) is proven has practically no cryptographic impact. This is because you can already write and execute algorithms (whose correctness depends on unsolved conjectures) without proving the conjectures. See http://math.stackexchange.com/questions/69540/would-a-proof-...

No. A proof is a nice thing to have, but everybody assumes that ABC is true already.

Initially I had the same concern, but after digging a bit deeper, I don't believe this would be an immediate outcome. From the little I can gather, the ABC conjecture is really just a statement about the relationship between the operations of addition and multiplication on triples of coprime positive integers. While prime factors are involved in the conjecture, it doesn't seem that the proof of the conjecture would naturally lead to prime factorization in polynomial time. I'm not a mathematician though, and given how radical Mochizuki's proof sounds, I imagine it may (if it stands) eventually lead to more efficient factorization algorithms.

Advances in computing power seem to be a more worrisome threat to RSA, especially for RSA-1024 whose factorization is probably already feasible (http://www.cs.tau.ac.il/~tromer/papers/cbtwirl.pdf). And once advances in quantum computing become reality, quantum algorithms should be able to very quickly break even RSA-2048 (http://en.wikipedia.org/wiki/Shors_algorithm).

Are there practical reasons we couldn't switch to RSA-65536?

Apart from cryptography, has prime number research and theorization produced any other practical applications?

Finite fields, essential to error-correcting codes, are based on properties of primes. This forms the basics of efficient data transfer, whether Internet, CDs or communication with spacecrafts. The book "Number Theory in Science and Communication" mentions that finite fields were used in verification of the fourth prediction of general relativity. See that book for more examples.

Here's one from http://mathoverflow.net/questions/2556: There is a gamma ray telescope design using mod p quadratic residues to construct a mask. Gamma rays cannot be focused, so this design uses a redundant array of detectors separated from the mask to reconstruct directional information.

Cicidas have a cyclic life spanning a prime number of years. It is supposed that this is because a predator has harder job aligning with the cycle. http://en.wikipedia.org/wiki/Predator_satiation

I believe that the Möbius function is important in advanced physics: http://en.wikipedia.org/wiki/Mobius_function#Physics

There's a legend that generals used the Chinese remainer theorem to count soldiers.

Elementary number theory was a motivating factor and foundation for development of the whole mathematics - algebra, analysis, even logic. Did you know that proving Godel's incompleteness theorem requires using primes? http://mathoverflow.net/questions/19857/has-decidability-got... Transcendence of pi also needs primes. http://mathoverflow.net/questions/21367/proof-that-pi-is-tra.... I did not realize that earlier. Usage of primes is often invisible. Even if there was no cryptography or ECCs, it would be silly to demand practical applications from this subject - it is a foundation for almost everything in mathematics, sometimes rather concealed.

By "practical application" I was also getting at other mathematics/physics laws/theories that are based on prime theory in some way. I guess you have highlighted a few.

Prime numbers can also be used to generate convincing pseudo-random numbers and patterns that don't repeat for long times.

You can basically use them whenever you need a number that has as few relations to other numbers as possible.

Anyway, as math is the language we use to model the universe around us, any mathematical property is likely to be a property of the universe in some way too (if maths is a proper model).

Apart from the single technology that allows open communication and allowed the Internet to e.g. become a business haven...

No, it should not.

Applications are open for YC Winter 2020

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact