# The End of Mathematical Proofs by Humans?

#### timothy posted about 9 years ago | from the somehow-I-doubt-it dept.

549
vivin writes *"I recall how I did a bunch of Mathematical Proofs when I was in high school. In fact, proofs were an important part of Math according to the CBSE curriculum in Indian Schools. We were taught how to analyze complex problems and then break them down into simple (atomic) steps. It is similar to the derivation of a Physics formula. Proofs form a significant part of what Mathematicians do. However, according to this article from the Economist, it seems that the use of computers to generate proofs is causing mathematicians to 're-examine the foundations of their discipline.' However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed. Defenders of the same point out that there are non computer-aided proofs that are also rather large and unverifiable, like the Classification of Simple Finite Groups. Computer-aided proofs have been instrumental in solving some vexing problems like the Four Color Theorem."*

## FP! (-1, Offtopic)

## Anonymous Coward | about 9 years ago | (#12151954)

## Re:FP! (-1, Offtopic)

## Anonymous Coward | about 9 years ago | (#12152020)

## Re:FP! (-1, Offtopic)

## Anonymous Coward | about 9 years ago | (#12152034)

## Science by AI (2, Insightful)

## MaDeR (826021) | about 9 years ago | (#12151955)

## Re:Science by AI (5, Interesting)

## FleaPlus (6935) | about 9 years ago | (#12152004)

Functional genomic hypothesis generation and experimentation by a robot scientist [nature.com]The question of whether it is possible to automate the scientific process is of both great theoretical interest and increasing practical importance because, in many scientific areas, data are being generated much faster than they can be effectively analysed. We describe a physically implemented robotic system that applies techniques from artificial intelligence to carry out cycles of scientific experimentation. The system automatically originates hypotheses to explain observations, devises experiments to test these hypotheses, physically runs the experiments using a laboratory robot, interprets the results to falsify hypotheses inconsistent with the data, and then repeats the cycle. Here we apply the system to the determination of gene function using deletion mutants of yeast (Saccharomyces cerevisiae) and auxotrophic growth experiments. We built and tested a detailed logical model (involving genes, proteins and metabolites) of the aromatic amino acid synthesis pathway. In biological experiments that automatically reconstruct parts of this model, we show that an intelligent experiment selection strategy is competitive with human performance and significantly outperforms, with a cost decrease of 3-fold and 100-fold (respectively), both cheapest and random-experiment selection.

New Scientist also had an article on it: "Robot scientist outperforms humans in lab." [newscientist.com]

## Re:Science by AI (4, Insightful)

## Zork the Almighty (599344) | about 9 years ago | (#12152009)

## Re:Science by AI (0)

## Anonymous Coward | about 9 years ago | (#12152026)

I imagine both will be a pretty tangled network of flesh&blood (natural or genetically engineered) and more traditional hardware.

## Yesterday's news? (0, Troll)

## nextdoornerd (845674) | about 9 years ago | (#12152080)

First, the story has been already discussed on technocrat.net day's ago (well, with 5 comments or so not really "discussed" as such :))

Second, I have to run to have lunch now and then boys... I'm eager to wrestle over my master's subject with the whole /. crowde... Oh, the sanity :)

Anyway, more to the point: it's not really AI, man. (At least nowadays.) Just some wonderfully pure math represented in (the most cases) painfully obfuscated, say, ML code >:\ (oh functionals, how I love thee... let me count the ways... uhm... zero? Ahemm.)

## Re:Science by AI (1)

## Squalid05 (850603) | about 9 years ago | (#12152152)

## I dress myself (-1, Offtopic)

## Anonymous Coward | about 9 years ago | (#12151956)

## Critics Reaction... (4, Insightful)

## Suhas (232056) | about 9 years ago | (#12151958)

if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands--impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed.So basically what they are saying is that if the proof is too long to be checked, then it is flawed? WTF?

## The Economist discussing math.... (0)

## Anonymous Coward | about 9 years ago | (#12151977)

If it were a math journal publishing this paper it might have some credibility.

But considering the source, it's just so a bunch of MBAs can feel smarter than PhD Mathemeticians for a while.

## Another Lomborg case? (2, Interesting)

## orzetto (545509) | about 9 years ago | (#12152133)

The Economist is the same magazine that supported Bjørn Lomborg [economist.com] , thereby proving their utter incompetence in environmental science. They defended him in spite of clear and very detailed indications [lomborg-errors.dk] from the scientific environment that he was nuts.

I suppose they will know economics when they talk about it, but they demonstrated an inappropriate habit of pontificating on things they don't have a clue about. I for one think they burned a lot of karma.

## Re:Critics Reaction... (5, Insightful)

## damieng (230610) | about 9 years ago | (#12151981)

If you can't independently examine and verify your "proof" then how can it be considered proof of anything?

## Re:Critics Reaction... (3, Insightful)

## wwahammy (765566) | about 9 years ago | (#12151982)

## Re:Critics Reaction... (1)

## oneandoneis2 (777721) | about 9 years ago | (#12151984)

...too long to be checked, then it is flawed?...You could be on to something here: That rule might apply to software too.

How many lines of code do they reckon make up the Windows source code..? :o)

## Re:Critics Reaction... (1, Insightful)

## Anonymous Coward | about 9 years ago | (#12151998)

## Re:Critics Reaction... (0)

## Anonymous Coward | about 9 years ago | (#12152017)

## Re:Critics Reaction... (1)

## Zork the Almighty (599344) | about 9 years ago | (#12152032)

## Re:Critics Reaction... (1)

## Tomfrh (719891) | about 9 years ago | (#12152088)

## Re:Critics Reaction... (4, Insightful)

## Zork the Almighty (599344) | about 9 years ago | (#12152116)

## Re:Critics Reaction... (3, Insightful)

## MonMotha (514624) | about 9 years ago | (#12152083)

I could assert that 2+2=4. You may believe me, but have I really proven it to you? Not yet, so you don't need to believe me. If I instead say that the the cardinality of the union of two disjoint sets, each of cardinality 2, is 4, then I've (sort of) showed you that 2+2=4, assuming you accept my definitions of disjoint sets, set union, and set cardinality (which presumably I've proven elsewhere, or taken from some other source). Now do you believe me that 2+2=4?

I could assert anything. You may or may not know if it's true. A proof is just something to back up my assertion and convince you that I'm right. Hence, if a proof is unintelligable, it's pretty darn worthless.

## Creativity (5, Insightful)

## Daxx_61 (828017) | about 9 years ago | (#12151961)

I for one welcome our new robotic theorum proving overlords.

## Re:Creativity (4, Funny)

## R.D.Olivaw (826349) | about 9 years ago | (#12151993)

## Re:Creativity (0)

## Anonymous Coward | about 9 years ago | (#12152036)

For me it was useful in showing what was possible and what wasn't. We would run programs to find "things" in projective spaces. Even if we did find something you would still be stuck in the position of 1) seeing if it is new, 2) proving that it was new (subtle but different). (Think of the symmetry groups of objects. If it has a big group then you would find quadrillions of these things; smaller the group less of them there are hence harder to find).

Generally exhaustive computer searches are impossible (you know, the amount of time before the sun goes medieval on our arses) for "interesting" problems . To make the computer searches feasible you need to think about the assumptions you need (starting configurations, symmetries etc) and then perform the search. The data you get back will give you some data points on where to do the next search. So "experimental mathematics".

## Hmpth (1)

## headkase (533448) | about 9 years ago | (#12152041)

Source [bartleby.com]

* A physical alteration thought to occur in living neural tissue in response to stimuli, posited as an explanation for memory.

Um. Yeah. Or something like that.

## Re:Creativity (4, Insightful)

## Zork the Almighty (599344) | about 9 years ago | (#12152092)

Without humans to drive the computers doing the work in the right directions, it could take a long time before a computer would be able to get its proof - it simply doesn't know what it is looking for.To some extent that's true, except in areas where human understanding has reduced mathematical proof to a mechanical process. For example, verifying algebraic identities, or even geometric proofs. A more advanced example is the Risch algorithm for elementary integration. It amounts to a proof that an integral either is or is not expressible in terms of elementary functions. Eventually we come to understand an area to such an extent that we can implement mechanical algorithms and move on. The proper role of the computer is to carry out these algorithms, so that we can use them to discover something else.

## R. Daneel? Is that you? (0)

## Anonymous Coward | about 9 years ago | (#12151963)

## If computers could write proofs... (4, Insightful)

## John Allsup (987) | about 9 years ago | (#12151965)

As a tool to produce vast quantities of precise logical porridge quickly, computers have no equal in today's world, yet that is not what real mathematical proofs should be about.

Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight. This is where computers will always be weaker.

## Re:If computers could write proofs... (2, Insightful)

## Dancin_Santa (265275) | about 9 years ago | (#12151989)

Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight. This is where computers will always be weaker.So you're saying that even a theoretical sufficiently advanced computer would be unable to match the logic and creativity of a human being? I think a simple brute force counter written in Mathematica (unlimited integer lengths) whose output was executed by a CPU would prove you wrong.

Computers can separate wheat from chaff. That's what AI is all about. No, seamless human interaction is still a ways off, but as for number crunching, the ability to compare large, disparate sets, and logical "thinking", computers are vastly more well-suited to the task than humans in every respect.

## Re:If computers could write proofs... (4, Funny)

## Hideyoshi (551241) | about 9 years ago | (#12151997)

## Re:If computers could write proofs... (1)

## Anonymous Coward | about 9 years ago | (#12152013)

Everything from load balancing to spam filtering to high-speed 3d graphics displaying uses AI to some extent. We used to call them expert systems, but you don't hear that term so much anymore because almost every system is an expert system of some kind.

## Re:If computers could write proofs... (1)

## lisaparratt (752068) | about 9 years ago | (#12152006)

## clever - yes, short - no (1)

## S3D (745318) | about 9 years ago | (#12152046)

Mathematical proofs should show short, clever ways of connecting otherwise disparate concepts that are only obvious in hindsight.Modern mathematics is very complex, important and useful theorems proven recently have huge and difficalt proofs, built from a lot of steps. Imortant results hardly have a short proofs.Take a look at the concepts used in the one of the most famous proofs of XX centery : the Feramt last theorem [wikipedia.org] . It's proof followed from the Taniyama-Shimura theorem [wikipedia.org] which establish non-obvious connection between quite different areas of mathematics. The proof is very long and complex, but of great importance for mathematics, and may have be realted to cryptography and even physics. Also such proofs are way outside of the power of near-future computers.

## Re:If computers could write proofs... (1)

## shanen (462549) | about 9 years ago | (#12152075)

Actually, I was officially a math major for about a year (before my transition to the much easier computer science). Some parts of it were pretty simple, but the proofs always threw me. I'd spend a couple of pages proving what I thought was the crucial step, and old Professor Bichteler would tell me that it was obvious, but the critical part was over here in the line between these two other steps, where I'd incorrectly thought it was obvious... Also, I had a tendency to prove almost everything by contradiction, and the professors wanted direct proofs. Which leads back to the original topic, since many computerized theorem-proving systems have favored proof by contradiction.

(However, the real reason I didn't become a better mathematician was probably the forced retirement of Professor Greenwood. He was a seriously great teacher, and I've always felt that a couple more classes with him would have made the difference...)

## If there are no proofs (0)

## willmeister (709686) | about 9 years ago | (#12151968)

## Seems simpler to prove proffs-by-computer (3, Insightful)

## Anonymous Coward | about 9 years ago | (#12151969)

To do that.... well, just make sure the program was designed by a correct computer.

## Re:Seems simpler to prove proffs-by-computer (5, Informative)

## rxmd (205533) | about 9 years ago | (#12152156)

## Does it really work? (1, Funny)

## janek78 (861508) | about 9 years ago | (#12151971)

## Re:Does it really work? (1)

## lisaparratt (752068) | about 9 years ago | (#12152019)

I hate prooving algorithms >_

## Godel/Turing/Cohen... (-1)

## ivano (584883) | about 9 years ago | (#12151976)

ciao

## Re:Godel/Turing/Cohen... (2, Informative)

## willmeister (709686) | about 9 years ago | (#12151996)

Why can't human brain functions be copied and improved upon in circuitry, other than the currently prohibitive costs involved, and our failure to accurately determine the exact neuron mapping of anyone's brain. Even the dynamic neuron connections could be potentially emulated or mimiced by a computer.

## Re:Godel/Turing/Cohen... (2, Funny)

## g1t>>v (121036) | about 9 years ago | (#12152049)

## Re:Godel/Turing/Cohen... (0)

## Anonymous Coward | about 9 years ago | (#12152090)

## Re:Godel/Turing/Cohen... (3, Insightful)

## Hideyoshi (551241) | about 9 years ago | (#12152018)

## Re:Godel/Turing/Cohen... (0)

## Anonymous Coward | about 9 years ago | (#12152044)

Parallel lines - those who's (minimal) distance from each other is the same at any points - indeed do not have some places where they touch and others where they don't.

If some silly mathemetician wants to publish a paper saying that he projected those lines on some curved space so now they touch - yet he still wants to call them parallel - that's a linguistics problem and not a math problem.

## Re:Godel/Turing/Cohen... (0, Troll)

## ivano (584883) | about 9 years ago | (#12152065)

There's absolutely no evidence that human minds have magical access to truths which formal systems don'tWhat has Penrose have to do with it? His little "quantum computers in our brain" has nothing to do with what I said. I gave you my sources: Cohen, Turning and Godel. That's it. Ask a logician if you don't believe me. All of these guys showed the limitations of formal systems (my bit about humans is irrelevant - and not very funny to begin with).

Ciao

## Re:Godel/Turing/Cohen... (0)

## Anonymous Coward | about 9 years ago | (#12152119)

dom

## Re:Godel/Turing/Cohen... (0)

## Anonymous Coward | about 9 years ago | (#12152081)

## Maths and computers? Who'd have thought (0)

## Anonymous Coward | about 9 years ago | (#12151979)

## Uh, I doubt it. (1, Insightful)

## Anonymous Coward | about 9 years ago | (#12151983)

Anyway, the entire point of a proof is to be read by humans. This isn't like, say, a computer program, where the point of the proof. A mathematical proof is something humans create in order to convince other humans of things beyond all doubt. The four color theorem proof was pretty closely watched; I guarantee you if you just go up to someone and say "statement [i]blah[/i] because my expert system verifies it to be the case" there is going to be some fucking doubt still there.

## Re:Uh, I doubt it. (1)

## g1t>>v (121036) | about 9 years ago | (#12152060)

## Here's a good theorem prover (4, Informative)

## carnivore302 (708545) | about 9 years ago | (#12151987)

## The best math is always elegant. (5, Interesting)

## Pants75 (708191) | about 9 years ago | (#12151988)

What about Fermats last theorem? Fermat wrote in the margin of his note book that he had a proof, but it was too large to fit there, so he'll write it on the next page. Trouble was, the next page was missing from the book.

The modern proof for FLT took hundreds of pages of dense math and went through some math concepts that AFAIK hadn't even been invented in Fermats time.

What was Fermats proof (if it existed)? It would surely have been far more elegant than the modern version.

That doesn't make the modern version wrong, just less pure, I feel.

The problem with modern computer aided proofs is they allow the proof to become unwieldy and overly verbose, compared to what it would have to be if just a human produced it.

Such is progress I guess.

## Re:The best math is always elegant. (1)

## wwahammy (765566) | about 9 years ago | (#12152010)

## Re:The best math is always elegant. (3, Funny)

## Craigj0 (10745) | about 9 years ago | (#12152015)

## Re:The best math is always elegant. (1)

## Pants75 (708191) | about 9 years ago | (#12152024)

I'd love someone who could test it to get hold of a copy though.

Tantalising.

## Computer _aided_ proofs (4, Insightful)

## irexe (567524) | about 9 years ago | (#12151991)

Computer proofs, like the graph color proof, are not proofs that are completely generated by a computer. The computer is merely used to brute force a fairly large number of 'special' cases which together account for all cases. The construction of the proofing method is and will remain human work, lest we create AI that matches our own I.In short, they are computer

aidedproofs only.Further and more importantly, at this point we do not have and are not likely to have a machine that can prove any provable theorem (and fyi, not all truths in mathematics are provable!).

## Re:Computer _aided_ proofs (2, Informative)

## g1t>>v (121036) | about 9 years ago | (#12152070)

## Re:Computer _aided_ proofs (1)

## ivano (584883) | about 9 years ago | (#12152076)

Ciao

## Incomputable math theorems (1)

## headkase (533448) | about 9 years ago | (#12152094)

reallycheck out Godel, Escher, Bach: An eternal golden braid [forum2.org] .This book basically describes Godel's incompleteness theorem [miskatonic.org] in an entertaining way for a general audience.

## very long proofs (0)

## bkubi (834026) | about 9 years ago | (#12152000)

## Re:very long proofs (0)

## StrawberryFrog (67065) | about 9 years ago | (#12152028)

can lead to different results than shorter ones, but both are correct.That to me is an extraordinary claim, and I'd like to see proof of it.

Anyone interested, read my favorite scince fiction author:Much as I like Greg Egan, fictoin is never a proof of anything. Because it's, you know, not actual.

## Are computer-aided proofs really proof? (3, Insightful)

## Mattb90 (666532) | about 9 years ago | (#12152001)

## Re:Are computer-aided proofs really proof? (0)

## Anonymous Coward | about 9 years ago | (#12152061)

my preparation for my interview to study Mathematics at Cambridge ...Whether many in the Mathematical community in England take this view, I won't know until the end of the year when I hope to start my course
Note that Cambridge is one of the leading places for computer-aided proofs [cam.ac.uk] .

## Re:Are computer-aided proofs really proof? (1)

## ockegheim (808089) | about 9 years ago | (#12152127)

## No progress without understanding (5, Insightful)

## Freaky Spook (811861) | about 9 years ago | (#12152002)

Although I discovered easier ways to do the arithmatic, I still knew the underlying theory of the equations & what the numbers were actually doing, not just what a computer was telling me.

Students should learn this, they are the basic building blocks of a science that dictates pretty much everything on this planet & although they won't have a use for everything they are taught they will have enough knowledge to "problem solve" which is what most of high school maths is designed to do, it trains our brains to think logically & be able to work out complex problems.

How are people going to be able to further phsyics, medicine, biology if they get into their respective tertiary courses without understanding the basic principals of all science & have to learn it all over again??

Or what about when computers just won't work & things have to be done by hand??

Its fair to integrate comuters into maths but not at the expense of the theory that makes us understand how things work, we should not put all our faith in technology just because its the easy thing to do.

## What about feigenbaum constant? (0)

## Anonymous Coward | about 9 years ago | (#12152003)

## Re:What about feigenbaum constant? (2, Interesting)

## Zork the Almighty (599344) | about 9 years ago | (#12152072)

## Theorem Proving (2, Interesting)

## NitsujTPU (19263) | about 9 years ago | (#12152025)

FOL Theorem provers jump through a number of hoops to make the whole bit a little more practical, but realistically speaking, having a computer that just runs through mathematical proofs in the manner that a human does is a long way off.

An interesting thing about the article is that the first proof was done with an FOL prover... it was a long, non-intuitive proof, but an FOL prover has performed that proof.

The second was done with code, a human had to write the program. There is no computer replacing the activity of a human in performing this action that I can see here. It was merely code to brute attack the problem from what I can see, but I didn't read the guys article (from what I can see, it hasn't reached publication yet anyway).

## Re:Theorem Proving (0)

## Anonymous Coward | about 9 years ago | (#12152121)

Theorem proving is NP Complete.You think so? Prove it. Or show us a proof.

## Elegant proofs (2, Interesting)

## erikkemperman (252014) | about 9 years ago | (#12152027)

But maybe there's a point where simple proofs just won't do it; if there were a 4 line proof for Fermat's last conjecture I'm sure someone would have found it before Andrew Wiles proved the thing in something like 80 pages.. In such cases, computer-aided reasoning is really the only way to go, I'd say. It's probably easier to verify a proofchecker than a proof.

## unverifiable (2, Interesting)

## StrawberryFrog (67065) | about 9 years ago | (#12152038)

However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed.Nonsense. If people can't verify proofs, then what you need to do is to verify them by computer

I'm not entirely joking here - so long as the verification program is written independantly of the thoerem-proving program, and it can reliably distinguish between valid and invalid logical inferences, what's the problem? It's simple automated testing methods really.

## Seems the computer is wrong (-1)

## MLopat (848735) | about 9 years ago | (#12152045)

"The four color theorem states that

every possible geographical map can be colored with at most four colorsin such a way that no two adjacent regions receive the same colour. Two regions are called adjacent if they share a border segment, not just a point."Well if you look at this political map of the United States [mapsofworld.com] it seems to me that Wyoming (or one of its surrounding states) would necessitate a fifth color.

So did the computer prove something true that isn't or is the theorem in the link provided simply stated wrong?## Re:Seems the computer is wrong (1)

## PakProtector (115173) | about 9 years ago | (#12152073)

## Re:Seems the computer is wrong (1)

## tgv (254536) | about 9 years ago | (#12152077)

No, this theorem is pretty valid, and it is intuitively understandable. The only problem is that the only existing proof is rather long...

## Re:Seems the computer is wrong (1)

## MLopat (848735) | about 9 years ago | (#12152079)

## Re:Seems the computer is wrong (0)

## Anonymous Coward | about 9 years ago | (#12152120)

Any map (on a flat bit of paper) can be coloured that way.

Now - it does NOT mean that given a pre-coloured map, you can't add areas that you can't colour. It just means that for those maps there was a DIFFERENT colouring which CAN be extended. You'll need to go back and recolour.

But it does seem to be true, after you play around with it for a while. It's not possible (on a flat bit of paper) to make an area which touches four other areas each of which touch each other.

Trying to do it, at some point you find that you have completely surrounded one of them, and you can then re-use that colour for your next area.

## Re:Seems the computer is wrong (0)

## Anonymous Coward | about 9 years ago | (#12152089)

I'm not going to answer for you, but please think.

Just because the state is surrounded by 6 states (which I'm guessing is your point) does not mean that 6 colours are neccesary.

For instance without considering the other states, these 6 could be represented by just 3 colours, while still following the rules.

Now think about what you have just said.

Please think.

## Re:Seems the computer is wrong (0)

## Anonymous Coward | about 9 years ago | (#12152093)

## Re:Seems the computer is wrong (0)

## Anonymous Coward | about 9 years ago | (#12152131)

Montana - Red

Idaho - Yellow

Utah - Red

Colorado - Yellow

Nebraska - Red

South Dakota - Yellow

North Dakota - Blue

I don't really see your point.

## Nothing too new? (2, Informative)

## xiaomonkey (872442) | about 9 years ago | (#12152050)

IIRC - back in the early days of AI (1960s), some people in the field thought that in relatively short order computers would be a major soucre of such mathematical proofs. It hasn't happened yet, but that doesn't mean that it won't eventually.

## Consider the source (-1, Troll)

## Qrlx (258924) | about 9 years ago | (#12152053)

What does The Economist know? It's a right-wing rag.

Wasn't always that way... sadly they're not what they used to be.

In terms of Slashdot, they would be posting at a 2. They've been around the block, but they're nobody special. Sorta like me.

## Re:Consider the source (0)

## Anonymous Coward | about 9 years ago | (#12152067)

## Re:Consider the source (4, Funny)

## Trogre (513942) | about 9 years ago | (#12152101)

What does The Economist know? It's a right-wing rag.What does Slashdot know? It's a left-wing rag.

## Re:Consider the source (1, Insightful)

## Anonymous Coward | about 9 years ago | (#12152153)

## Re:Consider the source (0, Offtopic)

## arodland (127775) | about 9 years ago | (#12152114)

## Re:Consider the source (2, Informative)

## l-ascorbic (200822) | about 9 years ago | (#12152123)

right wing ragthat backed Clinton and Kerry (albeit grudgingly), supports gay marriage, legalisation of drugs, gun control, abolishment of the death penalty..?## Re:Consider the source (4, Insightful)

## sien (35268) | about 9 years ago | (#12152125)

Secondly, the claim that a magazine that opposes the death penalty and supports gay marriage is right-wing rag (which presumably you meant in US terms, is kinda amusing.

The Economist, correctly stated, is a liberal magazine. It supports liberal economics and liberal social policy. Unfortunately the word 'liberal' in the US has been badly distorted.

## Re:Consider the source (0)

## Anonymous Coward | about 9 years ago | (#12152129)

They've been around the block, but they're nobody special. Sorta like me.By virtue of your posting here on

## Re:Consider the source (0)

## Anonymous Coward | about 9 years ago | (#12152134)

## Stupid post name (1, Insightful)

## Anonymous Coward | about 9 years ago | (#12152058)

The article is about computer-aided proof, where the human makes the essential proof decisions while letting to the computer the tasks of properly formulating and performing very simple, yet laborious steps (which would otherwise draw the attention of the human from essential stuff).

You **cannot** actually prove a really complex theorem in a fully automated way, because the reasoning is non-monotonic, which implies huge computational complexities. Machines are not yet good at being creative.

## Blowhard critics could use a logic course... (4, Insightful)

## geekpuppySEA (724733) | about 9 years ago | (#12152096)

However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed.Because if there's one thing that humans are better at than computers, it's performing large numbers of repeated steps. Flawlessly.

## here y'all go again, panicking... (3, Insightful)

## Fry-kun (619632) | about 9 years ago | (#12152115)

It's easy to check a proof. It's hard to come up with a proof. Computers are great at checking proofs - all the program needs to do is verify whether the steps are logically correct or there's a discrepancy. Coming up with a proof, on the other hand, is a very hard task (being NP-complete, unless defined in a certain way) and thus usually requires a human (or sometimes, a lot of humans) to work on the problem.

A computer would not be able to come up with new principles of mathematics in order to tackle a given problem, it would only try to use every trick that has been discovered to the point of creation of the program (of course that doesn't have to be the case, but my point is that human intervention would be required to "teach" the computer about the new concept so that it would try to use it for the proof)

That is not to say that computers are useless in proofs. Obviously, they're often used as assistants in proving something-or-other, but there's also a direction in computer science where your computer would take a program that you wrote in a certain manner, and prove certain properties about it, e.g. that it is not possible to get out of array bounds in your C program...

*yawn*

time to sleep

## A proof needs to be intuitive (4, Informative)

## nigham (792777) | about 9 years ago | (#12152135)

I doubt the human proof system will go away completely - even if we can check nasty theorem proofs using computers, we still need humans to sit and explain what they mean.

## Change roles? (1)

## archeopterix (594938) | about 9 years ago | (#12152138)

Such proof verifiers already exist today, but they are too stupid to be used to verify non-trivial theorems. They don't understand such paper-savers as "... other cases follow from this one" or "without loss of generality...". Of course, to allow such statements and still honestly check the proof, the verifier would have to generate some trivial parts of the proof itself - this is what human readers of mathematical papers do routinely. Are we thus back to square one (verification -> generation)? Well - proving the lemmas may be hard, but I think it's still much simpler than generating non trivial proofs.

## Subject (1)

## Legion303 (97901) | about 9 years ago | (#12152140)

## proofs?? (1)

## Androk (873765) | about 9 years ago | (#12152147)

## There's always room for creativity. (1)

## bombadier_beetle (871107) | about 9 years ago | (#12152148)

## The one main advantage of computers... (1)

## boris_the_hacker (125310) | about 9 years ago | (#12152149)

I am currently hand proving some logic for my phd and it is a pain in the arse. I also have a tool that I have written to do the same thing.

I still have to prove the logic is correct (by hand) and that the tool implements the proof search correctly (trickier) so I can then use the tool to solve bigger problems.

Some of the proofs the program generates in under a minute takes myself days to do. (50+ pages of pdf generated from LaTeX).

Through the development of the tool, I could validate from my hand written proofs whether it was generating correct proofs. Sometimes it would get things wrong and others it would do it better than myself.

Computers are useful but only when we hardcode them with understanding that we have developed.