Wikipedia-size maths proof too big for humans to check | Hacker News Reader

Wikipedia-size maths proof too big for humans to check

newscientist.com

39 pointsgraeham60 comments

So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute.

Alas, such a proof throughly fails the second test. I can't see how to gain insight into the problem from such a proof, beyond just it validating previous thought chains of the form "If X were true, then I could deduce Y". It doesn't reveal more about the structure of the problem, or other results in the space.

It's no doubt useful (and all credit to the authors), but in terms of generating new mathematics, I'm dubious. Perhaps people more versed in this specific sub-field can tell me if I'm wrong?

It is a field of AI, not a field of Mathematics.

Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician.

At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct.

http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...

I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations.

In Haken and Appel's proof there was no automated reasoning.

Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2.

To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.

All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal.

The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations.

Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods.

http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...

Knowing the FCT as well as I do, I have to say that I and many of my colleagues do not consider the H-A proof to be anything like automated reasoning. The work that Gowers and associates are now doing is very much so, but programming a computer to conduct a specific search, and for every item found compute whether it has a specific characteristic is really just like getting a machine to carry out a factoring algorithm.

We run the risk of arguing past each other, and potentially being in "violent agreement," but consider this. If you take an 8x8 chessboard and remove any black square and any white square, the resulting mutilated chess-board is guaranteed to be exactly coverable by dominoes, each of which covers exactly two squares. We can program a computer to conduct an exhaustive search to show that this is true. Would you consider the program to be an automated reasoner?

With what I know of this recent result, the work seems equivalent. It's a big problem fed to a SAT solver.

Edit: See the last paragraph of section 1 in the paper: http://arxiv.org/pdf/1402.2184.pdf

Yes, although brute force would be "simple AI", but the basics of AI nonetheless.

One of the many "classic" problems given to students of Artificial Intelligence is the 8-Queens problem: http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in...

It is a short step to go from "8-Queens Algorithm Design" to "8-Queens Logic Programming", and from there automated reasoning. After all, Logic Programming is purely based on automated reasoning using Horn Clauses. It just so happens to be one of the most optimized forms of automated logic, fast enough to be a general programming language (Prolog is one of the easiest languages to solve the 8-Queens problem)

Automated Reasoning covers new tricks, like tree pruning, different logic systems or methodologies (Tableau Logic)... but no matter how complicated it gets, it all comes back to the same methodology. Its simply a glorified search algorithm, defined over some space. (Prolog at its core is nothing more than a depth first search over the horn clauses specified by the programmer)

For an example that clearly demonstrates the search, here's a Wikipedia link to Tableau type automated reasoning:

http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Sea...

And of course, the Automated Conference on the Tableaux Automated Reasoning methodology:

http://en.wikipedia.org/wiki/International_Conference_on_Aut...

The "Art" of Automated Reasoning is not in the search methodology (which is almost always just depth-first search + heuristics), but in how to define those spaces. Horn Logic, Tableaux, First Order Logic / Resolution Rule, etc. etc.

So whenever a new "search space" is defined to solve a practical problem, it is always of great interest to the Automated Reasoning community.

  >> If you take an 8x8 chessboard and remove any
  >> black square and any white square, the resulting
  >> mutilated chess-board is guaranteed to be exactly
  >> coverable by dominoes, each of which covers exactly
  >> two squares. We can program a computer to conduct
  >> an exhaustive search to show that this is true.
  >> Would you consider the program to be an automated
  >> reasoner?
	
  > Yes,

That surprises me. That feels a lot like describing Eliza as a conversationalist. Technically true, but ultimately unhelpful and unenlightening.

By way of contrast with the above described brute-force search, which also only works on a fixed size board, here's a proof that works on all NxN boards, where N is even.

We can construct a tour of the squares, visiting each exactly once, each time moving from a square to one of the squares with which it shares a side. Removing one black and one white divides this into two (or possibly only one) segments. Each can easily be shown to be of even length, and therefore each is coverable by dominoes. QED.

If you simply enumerate a very large number of possibilities, it doesn't feel like reasoning.

I think you two are disagreeing about terminology. You're the ecpert in the field, which (correctly) makes you more sensitive to terminological distinctions.

What's not disputed I guess, is the commonly (to CS-educated engineers) held notion that FCT is a high-profile math problem that was solved/proved by intensive automatic means rather than a human written proof, and that that raises questions regarding the meaning of "proof".

At least that's what I took home from it.

Other people claim that FCT was proven by computer. Most of my colleagues say it was proven by Haken and Appel, who programmed a computer to perform a finite search. People who work in the area - including me - say it's like getting Wolfram Alpha to solve your integrals, while you do the actual thinking about what integrals need solving, why, and what to do with the answers.

I see what you nean: the computer as a tool, rather than as the one that does tge proving.

“Computers Are Useless. They Can Only Give You Answers” -- Pablo Picasso

You seem to be of the opinion that only "Strong AI" should be considered as "intelligence". In contrast, I'm of the opinion that "weak AI" is sufficient for the "intelligence" definition.

Although, since I've done some research in the AI Field, I also recognize the distinction and the two. There is a controversy, even in AI circles, over what constitutes AI. So I'm not going to debate with you the merits of Strong AI vs Weak AI.

It is sufficient enough for me to just inform you... this controversy exists and is real.

---------------------------

http://www.i-programmer.info/babbages-bag/297-artificial-int...

>>> This is the curse of strong AI. Whenever you make something work, you know how it works and it no longer seems intelligent.

I don't claim to be better versed in this field, but a way forward could be to do common subexpression elimination on this proof. Then, try and give names to those common subexpressions.

Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.

I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value.

I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem.

To me, what you say makes no sense at all. Perhaps this is what the field needs - people who know absolutely nothing making suggestions that are so far outside the box that those who have spent decades studying it would never consider them.

On the other hand, maybe there's nothing in it. Have you thought it through more? Do you have more ideas? Do you have any actual concept of what "sub-expressions" might mean in this context? Having written compilers for food I feel that I have some knowledge of the concept, but in this case it seems not to mean anything.

I wonder if you misunderstood his comment as a suggested method to solve the mathematical problem?

The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.

The question then is whether there's any exploitable semantic structure in the certificate. I would guess not, but I don't have enough knowledge of the specifics of this problem and proof to be more certain. It just doesn't feel likely - any structure would emerge in the way the sub-sequences could be constructed, and lack of such structure is what makes this problem hard.

Just a guess.

When he says "sub-expressions", he means it in the program-code sense. Really, he's saying: why don't we try to refactor the proof?

And, since it's so large, we probably can't do it by hand. So we would need to develop techniques to do it automatically. (Or semi-automatically.)

But the proof isn't large, just the output of the search. Assuming my understanding of the problem and the result are correct, the reporting on this is so poor as to be meaningless and misleading. As such, the comments are well-meaning, but (to me) seem meaningless.

Of course, my "understanding" may be completely wrong.

Let's avoid the use of the word "proof", which I address above. Is it possible to do any analysis of the output of the SAT solver, the certificate, to gain any insight into the problem? That's what the poster was asking.

Using that context, I have no knowledge of the form the certificate takes, so I can't venture an opinion at all in this case. I suspect the answer is "no", but that's just on general principles.

These theorem provers receive as input a high level computer program that describes how to generate the proof and output a low level sequence of logical steps. I think looking at that high level input is going to be more helpful then trying to reconstruct it from the output.

In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?

and now we're into questions about homoiconicity. I think I see why Lisp was so popular in AI research.

Because the output of the program is effectively a long list of cases of things that have been considered[0], and why they do or don't "work" in some sense. The output is independent of the program and, in principle, can be checked. In some ways it's like printing the search tree of chess to show that white has a forced win. It doesn't matter if the program is "correct" - you can check the output separately.

[0] EDIT: actually it's the certificate from a SAT solver

I believe "Someone" is wondering whether it's possible, and if so helpful, to work out the common factors in those search trees and give them names, much as a certain chess search tree could efficiently be called "Stonewall White" if it represented all boards reachable from that class of opening.

I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?

A CS prof I had held the position (in grading his tests - perhaps not generally) that "a proof is anything that convinces me you could write a proof". The program, along with an output saying "true", would seem to suffice under that metric.

It's a certificate output by a SAT solver. More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray. Verifying the hardware and software isn't enough.

And yes, the whole question is to ask to what extent we can trust this. Personally, it's just as likely that a human proof would have a subtle and hard-to-find error, missed by all the reviewers.

All the popular articles are claiming this humungous output is a proof. It's not a proof, it's a certificate from a SAT solver. There's a difference, and most comments people are making based on the popular accounts are misguided.

> More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray.

Hmm. Are bit flips from cosmic rays more likely than a human making a mistake verifying a proof, or even a large number of humans making the same mistake?

If one human makes the mistake, it's probably because it's a mistake that humans trained in this field are likely to make. Mistakes are not independent in this sense. Also, the number of humans capable of an in-depth analysis of the result is small, and they've mostly all got the same training, so if there's a subtle mistake, it's one to which they are all susceptible.

If the certificate from the SAT solver does not count as a proof, you can't blame the popular accounts. That's the language the paper authors use:

The negative witness, that is, the DRUP unsatisﬁability certiﬁcate, is probably one of longest proofs of a non-trivial mathematical result ever produced. Its gigantic size is comparable, for example, with the size of the whole Wikipedia, so one may have doubts about to which degree this can be accepted as a proof of a mathematical statement.

From http://arxiv.org/pdf/1402.2184v2.pdf

I think the problem is that the general public think of "proof" as the kind of thing that mathematicians sit and work out with a pencil on paper. To use the word "proof" to refer to a certificate is technically correct and appropriate in context, but deeply misleading when used outside of that context. It certainly gives the wrong impression.

I also suspect we're mostly in complete agreement.

What's the difference between a certificate and a proof?

It takes a human to look at the certificate, to understand WTF was just solved by this program, and then demonstrate that the certificate actually lines up with the math problem.

>More, you can't guarantee that there wasn't a bit flip caused by a cosmic ray.

You could just run the program and verify that the certificates match a few times, I guess you can't be 100% certain but the probability of a bit flip happening multiple times is extremely small.

Why can't it check for bit-flipping along the way and such like using techniques similar to error correction codes. And do every calc at least three times or something. Come on people, you're letting the side down!

Absolutely - you seem to have nailed every point.

The only thing you've missed is this - we now know that for C=2 the minimal length required to force a sub-sequence of discrepancy >=2 is 1161. The technique used gives a hint of how fast this dependency might grow, and that might give clues about techniques that probably won't work.

It also seems clear that a similar brute-force check of C>=3 won't be possible. Knowing these things gives clues as to how we might now proceed.

Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?

Presumably nothing. Unless you know how to program strong AI, and even then it probably wouldn't find anything interesting. There is no definition of what "interesting" is. It could discover tons of truths like "555 + 724 = 1279" but none of those would be particularly interesting to humans.

Perhaps an infinite number. However, like a tree falling in the woods ... if humans (or some other intelligence) can't understand it, has anything actually been discovered? Or is it more like a computer algorithmically solving a jigsaw puzzle?

What what? And, what the hell is an infinite number?

That would prove to be insurmountably difficult:

http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...

It would "discover" every curiosity that we have yet to find, but it would be useless.

Consider the universe. It is essentially a giant mechanical construct which works within the confines of every mathematical, physical, and even metaphysical truth.

Imagine that you don't exist. Then what can you learn from the universe? The universe itself might "discover" everything. But that is meaningless to you. Now assume you do exist in the universe. What truths does the universe teach you? Only the ones that you witness and understand.

If I come up with an incredible proof and write it down on paper and put it in my shirt pocket. Then I don't tell anyone until I die, and I'm cremated in the same shirt with the same proof, and my ashes are scattered across the ocean, what have I discovered? I only discovered something that was already true, I didn't bring the truth into existence, and while I didn't do anything with it nor share it with anyone it doesn't mean that it became any less true. But then what was the purpose?

The purpose of a proof is to take a truth and to distill it into an idea that can be shared. A truth on its own is meaningless. If I say a^2+b^2=c^2, a lot of context is required, what do a, b, c mean? What sort of geometry does this work in? Why is this the case? Is it ever not the case? When every question is answered, and you are certain of that, then you have a proof. Just knowing that a^2+b^2=c^2 is meaningless. Even if I could prove that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse, that's still not completely meaningful, because it's not true in elliptic or hyperbolic geometries.

But the abstract idea, that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse is Euclidean space is meaningful, because it leads to questions like "What would that mean about space if the sum of the squares of the lengths of sides of a right angle triangle were greater or smaller than the square of the hypotenuse?" and you start to consider alternative geometries.

If a computer were to definitively prove that a^2+b^2=c^2 what does that mean if you can not really understand the implications of the proof. Yes it's true, but what does it mean? And why?

But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost say) how much more likely you are to prove something else (or how much easier it would be) -- without computer assistance.

But the twist is that with computer-aided proofs, being well-versed in the ways of using computers to help prove things may begin to count as having insight; and Coq (or whatever) programs may come to be studied so that one may gain insight, just as human proofs are studied today.

The case analysis demonstrates that the overall nontrivial strategy is correct.

The insight is in the strategy.

A good mathematical proof is like a poem, not a telephone directory.

https://hn.algolia.com/?q=proof#!/story/past_week/0/maths%20...

Those submissions never got traction or comments, why link them?

Because sometimes older submissions end up getting some discussion, even when more recent submissions have more comments.

http://www.reddit.com/r/math/comments/1y5v15/if_no_human_can...

"Wikipedia-sized" Is it really? They say in the article that the text of Wikipedia is a 10GB download, but that has to be compressed (and compression on plaintext, which comprises most of Wikipedia, is extremely efficient). I'm guessing (but have no proof) that their 13GB file was raw data.

A minor thing, but comparisons like this always drive me nuts. Just say "13GB proof too big for humans to check." Then there's no confusion.</sillyrant>

A lot of its name games. 10 gigs of possibilities tested is actually pretty short for something like OGR-27. We're probably going to prove OGR-27 in a few weeks (or has it already been announced?) and I'm fairly certain a list of all possible rulers checked would exceed 10 gigs. Yet you can report OGR-26 in only 26 small numbers, or I guess you could draw a graphic pix using 492 pixels or whatever.

So is OGR-27 merely 27 numbers aka a 1-d pixel "graph" probably around five hundred something pixels, or is it really zillions of gigs of rulers all of which are longer than the OGR?

"Wikipedia" is displacing "encyclopedia" and "Library of Congress" as a unit of measure!

Clearly there is a defent "yo mamma" joke in there.

Uh, and football field. The output of this proof if laid end to end would fill 37 regular sized football fields.

"The set-theoretical axioms that sustain modern mathematics are self-evident in differing degrees. One of them – indeed, the most important of them, namely Cantor's axiom, the so-called axiom of infinity – has scarcely any claim to self-evidence at all". John P. Mayberry

From the linked Wikipedia article:

> All experiments were conducted on PCs equipped with an Intel Core i5-2500K CPU running at 3.30GHz and 16GB of RAM.

Why are these experiments not being conducted on a more powerful computer or a cluster?

Because it only took 6 hours anyway.

As already mentioned, it only took six hours. To make it run on a cluster or supercomnputer, you must parallelize the algorithm, which will take considerably longer time, even if it is easy. Then they likely have to apply for access, which also take time. Then it is easier to just run it on an available computer.

For the same reason you don't see word processors using a more powerful computer or cluster to render text for display as pixels.

- It would be awfully inconvenient to program

- It would require buying, building or obtaining access to such a machine

- It'd require investing some amount of time and/or money -- obviously completely unnecessarily -- because whatever desktop or laptop happened to be within reach is perfectly adequate to the task

Reply on news.ycombinator.com