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

61–65 of 65 posts

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

#61

Post by wlievens »

ColinWright wrote: post #60
wlievens wrote: post #56

Earlier quoted context omitted.

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.

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

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

#62

Post by adiM »

ColinWright wrote: post #60
wlievens wrote: post #56

Earlier quoted context omitted.

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.

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

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

#63

Post by dragontamer »

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…

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.

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

#64

Post by csense »

adiM wrote: post #5

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?

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

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

#65

Post by lovemath »

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…

A good mathematical proof is like a poem, not a telephone directory.
Post reply on HN