Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Wikipedia-size maths proof too big for humans to check

newscientist.com

Post reply on HN
Print view View original

51–60 of 65 posts

Re: Wikipedia-size maths proof too big for humans to check

#51

Post by zeidrich »

brador wrote: post #22
archgrove wrote: post #4

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…

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

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?

Re: Wikipedia-size maths proof too big for humans to check

#52

Post by dragontamer »

judk wrote: post #47
ColinWright wrote: post #38

Earlier quoted context omitted.

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…

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.

Re: Wikipedia-size maths proof too big for humans to check

#53

Post by ColinWright »

scott_s wrote: post #45
ColinWright wrote: post #33

Earlier quoted context omitted.

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.

Re: Wikipedia-size maths proof too big for humans to check

#54

Post by ColinWright »

dragontamer wrote: post #41
ColinWright wrote: post #34

Earlier quoted context omitted.

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 algorith…

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 bas…

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

Re: Wikipedia-size maths proof too big for humans to check

#55

Post by wlievens »

arbitrage wrote: post #29
brador wrote: post #22

Earlier quoted context omitted.

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

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?

Re: Wikipedia-size maths proof too big for humans to check

#56

Post by wlievens »

ColinWright wrote: post #54
dragontamer wrote: post #41

Earlier quoted context omitted.

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 bas…

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

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.

Re: Wikipedia-size maths proof too big for humans to check

#57

Post by igravious »

ColinWright wrote: post #38
baddox wrote: post #35

Earlier quoted context omitted.

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?

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…

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!

Re: Wikipedia-size maths proof too big for humans to check

#60

Post by ColinWright »

wlievens wrote: post #56
ColinWright wrote: post #54

Earlier quoted context omitted.

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

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 meanin…

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.
Post reply on HN