Computer Generates Largest Math Proof Ever At 200TB of Data (phys.org) 143
An anonymous reader quotes a report from Phys.Org: A trio of researchers has solved a single math problem by using a supercomputer to grind through over a trillion color combination possibilities, and in the process has generated the largest math proof ever -- the text of it is 200 terabytes in size. The math problem has been named the boolean Pythagorean Triples problem and was first proposed back in the 1980's by mathematician Ronald Graham. In looking at the Pythagorean formula: a^2 + b^2 = c^2, he asked, was it possible to label each a non-negative integer, either blue or red, such that no set of integers a, b and c were all the same color. To solve this problem the researchers applied the Cube-and-Conquer paradigm, which is a hybrid of the SAT method for hard problems. It uses both look-ahead techniques and CDCL solvers. They also did some of the math on their own ahead of giving it over to the computer, by using several techniques to pare down the number of choices the supercomputer would have to check, down to just one trillion (from 10^2,300). Still the 800 processor supercomputer ran for two days to crunch its way through to a solution. After all its work, and spitting out the huge data file, the computer proof showed that yes, it was possible to color the integers in multiple allowable ways -- but only up to 7,824 -- after that point, the answer became no. Is the proof really a proof if it does not answer why there is a cut-off point at 7,825, or even why the first stretch is possible? Does it really exist?
Yes. (Score:5, Insightful)
Re: (Score:1)
The question was actually asked by Bob Yirka, the reporter of TFA on phys.org.
But yeah.
Re:Yes. (Score:5, Interesting)
Indeed. I'm rather confused by the editorial commentary. To put it in terms of the summary regarding a question of color, imagine if someone asked the question, "What color is the sky?" Conjecture: The sky is blue.
Proof? Point an instrument at the sky and measure the light coming from it. Looking at the spectrum of frequencies coming from the sky, it falls into a range of colors that humans would generally associate with "blue."
That's it -- you've "proved" what the color of the sky is, i.e., "blue."
TFS instead starts asking, "But WHY are the frequencies emitted from the sky in the range that qualifies as blue? Why aren't there other dominant frequencies? Why do they fall in a particular range? Have we really proved what color the sky is???"
These are all very interesting questions, but they are irrelevant to the fact that the sky IS blue and one can prove it by measuring the frequency and correlating it with what humans call "blue." Proofs aren't generally about "why," and in fact many concise "elegant" mathematical proofs may be completely non-intuitive about showing why they work -- nevertheless they are considered valid proofs.
Re: (Score:2)
Re:Yes. (Score:5, Funny)
Dude, we all know that if you keep digging these "why" questions, you'll just end up with 42.
Re: (Score:3)
42... A very finite number indeed.
And therein lies the problem - Is it possible to demonstrate a proof through brute force?
Re: (Score:2)
"Is it possible to demonstrate a proof through brute force?"
Yes.
Prove that the number of unique permutations of the first 3 natural numbers greater than 0 is 6.
Proof:
1 2 3
1 3 2
2 1 3
2 3 1
3 1 2
3 2 1
QED
Re: (Score:3)
For certain classes of proof, yes.
These classes are ones where the solution space is finite, in which case one can merely enumerate through all the possibilities. Another is where you're proving in general something is true - like in this case. In which case all you need to do is find one counter-example to prove the hypothesis wrong. Which happened here - they simply went through and enumerated the possibilities and checked each and every one of the
Re: (Score:2)
42... A very finite number indeed.
And therein lies the problem - Is it possible to demonstrate a proof through brute force?
For classes of problems whose solution space are finite, then yes, it is possible, and in many cases, desirable. If the solution space has properties similar to a finite subset of, say, the natural numbers, then you could prove by induction. Depending on the situation, some of these problems are easier to prove via induction, and other times, by simply iterating over the problem space.
Re: (Score:2)
I thought the answer was anything to not go through a bunch of color swatches to pick a new color for the living room...
Re: (Score:2)
Rayleigh scattering? I think it might actually be a bit more complicated than you think. [xkcd.com]
Re: (Score:1)
That's it -- you've "proved" what the color of the sky is, i.e., "blue."
Perhaps you've proved the frequency of the color from the sky, but are you sure the definition of blue to include this particular frequency for this object is correct definition of blue? Perhaps not.
Re: (Score:2, Insightful)
It is upon the asker to define what would qualify as blue. Otherwise the problem is underspecified.
Mathematical Proof != Scientific Theory (Score:5, Interesting)
These are all very interesting questions, but they are irrelevant to the fact that the sky IS blue and one can prove it by measuring the frequency and correlating it with what humans call "blue."
This is not a mathematical proof but a scientific theory supported by evidence. A mathematical proof, if correct, is always and absolutely true. The major difference is that suppose I did your experiment at night, or at sunrise/sunset, or on a cloudy day? I could get red, black, white or grey for the colour of my sky. All you can do in science is take data, come up with a thoery to explain that data and then test the predictions of that theory under conditions where nobody has tested it before to see whether it works. In your case it is very easy to disprove the theory that the sky is blue.
In fact you can never really prove a scientific theory - all you can say is that it works in all the situations it has been tested under. That's good enough to be extremely useful and to advance our understanding about how the universe works but it is not the same thing as a mathematical proof. This is why scientists spend time confirming that existing theories work in new situations but you never hear of mathematicians checking the pythagorus theorem again to confirm that it still works with new right-angled triangles.
Re: (Score:1)
This is not a mathematical proof but a scientific theory supported by evidence.
I knew somebody was going to come and start arguing about this nonsense. Look -- I was trying to make a rough analogy in common language, first of all, which should have been clear to anyone (I thought). OBVIOUSLY the statement "the sky is blue" is not true at night or when it's cloudy or whatever. Duh. Thanks, Captain Obvious.
A mathematical proof, if correct, is always and absolutely true. [snip] In fact you can never really prove a scientific theory - all you can say is that it works in all the situations it has been tested under.
I want you to think hard about this. This is a common statement, but if you actually spend some time interrogating what you're claiming, you'll realize there is no PRACTICAL diff
Re: (Score:1)
Mathematician and former research scientist here. (Sorry, I always post AC just on principle, so you'll have to verify everything I say from other reputable sources, not an online reputation.)
This post was just asking for a rebuttal. And in fact, I've trimmed up my rebuttal to just this tl;dr version:
Math: Logically provable theorems which apply only to the set of rules they were written for. You cannot perform a mathematical "experiment." Proofs can be logically flawed by making invalid assumptions. You wi
Re: (Score:2)
Look -- I was trying to make a rough analogy in common language...OBVIOUSLY the statement "the sky is blue" is not true at night or when it's cloudy or whatever. Duh. Thanks, Captain Obvious.
Sometimes when dealing with General Ignorance you have to be Captain Obvious although here apparently not obvious enough. I understood your rough analogy for what it was and was extending it to explain to you the difference between a scientific theory and a mathematical proof. It doesn't matter what scientific statement you make you can never prove it is always true under all circumstances. The best you can say is that every time you have tested it the statement has proved to be correct.
So, you're stuck with a couple of possibilities...
No actually you ar
Re: (Score:2)
Sometimes when dealing with General Ignorance you have to be Captain Obvious although here apparently not obvious enough.
Woah -- sorry, but that's over the line. I admittedly was a bit rude in making fun of your post, and for that I would apologize. But I did not accuse you yourself of being an idiot. This is impolite and unwarranted. If you spend even a few minute reviewing the history of my posts here, you'd know that I have a deep background in the history and philosophy of science. So accusing me of "general ignorance" in this area is really being a jerk.
Nevertheless, I'm in a good-natured mood, so I'll respond a b
1980s all over again (Score:2)
Mathematicians initially rejected the idea that this constituted a mathematical proof for the r
Re: (Score:3)
Re: (Score:2)
Re: (Score:2)
Point an instrument at the sky and measure the light coming from it. Looking at the spectrum of frequencies coming from the sky, it falls into a range of colors that humans would generally associate with "blue."
Or, you know, just look at it and observe that it is blue.
Re: (Score:2)
Indeed. I'm rather confused by the editorial commentary. To put it in terms of the summary regarding a question of color, imagine if someone asked the question, "What color is the sky?" Conjecture: The sky is blue.
Proof? Point an instrument at the sky and measure the light coming from it. Looking at the spectrum of frequencies coming from the sky, it falls into a range of colors that humans would generally associate with "blue."
That's it -- you've "proved" what the color of the sky is, i.e., "blue."
Which illustrates the naive idea of what a proof is: a bit confused. For one thing, mathematical proof does not work this way - what comes closest, conceptually, is a physical experiment, but it fails, in the sense that the purpose of an experiment in empirical science is not to prove something; at best you can hope to disprove, or if you fail convincingly in doing that, you can confirm you theory. But a proof it aint. Only mathemetics can provide positive proof of anything, and only because it restricts it
Re: (Score:3, Interesting)
Well, let me take the devil's advocate position for a moment.
Yes, it proves the conjecture, but by relying upon a mechanical process you miss out on something that is required by humans to bring the problem within the grasp of our limited attention spans and working memory: insight. So we know the answer to the conjecture, but it doesn't advance our understanding of the problem and its related problems the way a human proof would.
So you could say it's proof of the conjecture in the sense that it's convinc
Re:Yes. (Score:4)
So you could say it's proof of the conjecture in the sense that it's convincing evidence of the truth of the conjecture. But it doesn't necessarily contribute to mathematical knowledge in the same way you'd expect a traditional proof to. So you could well look at it as a "proof" but in only a restricted sense.
I'm not sure how enumerating a finite set and demonstrating that a property holds for all its elements (or conversely, that it doesn't hold for some of its elements) doesn't constitute "a traditional proof". Dealing with finite cases by enumerating them seems perfectly traditional to me.
Re: (Score:2)
No! (Score:1)
Rethink!
Do you need a human to confirm most precise calculations of pi? No. You need the human to confirm correctness and appropriateness of the software that does so, or of software which itself ensures correctness (and still the human must check appropriateness - basically, is the algorithm mathematically sound).
Re:Yes. (Score:5, Insightful)
That's not even true of many traditional proofs. Some traditional (i.e., by humans) are long enough to require weeks to months of study, as well as years to produce.
This is more extreme in that nobody can reasonably go over that much proof, no matter how dedicated they are, but in principle it could be done by overlapping teams of people. It won't be, because people don't doubt it sufficiently. Various people will look at various parts of the proof. But it *could* be done.
There's one math proof that's been published for over a year (forget what it's about, or how much over). It's by one mathematician, not by a computer, but it was developed over a decade or so, and he developed some eccentric tools that aren't widely understood, so verifying the proof requires significant work, and hasn't been done. Will it be done? Is it as trustworthy as a proof by a computer that also hasn't been gone over in detail by lots of (other) mathematicians?
The problem isn't just computers, it's a degree of complexity beyond what most professional mathematicians are prepared to deal with. And it's showing up in several places around the edges of various fields.
Re: (Score:2)
That's not even true of many traditional proofs. Some traditional (i.e., by humans) are long enough to require weeks to months of study, as well as years to produce.
There's a major difference between 'require weeks to months of study' to review VS Time to Read VS It would not be physically possible for you to read this in your lifetime!
The problem isn't just computers, it's a degree of complexity beyond what most professional mathematicians are prepared to deal with.
Greater complexity can also lea
Re: (Score:2)
And not only read the source, but re-run the source yourself.
Or write your own program to validate the output of the first.
Even a "simple" proof that sums a long list of numbers would be unfeasible for a human to add up and check, yet we would all feel comfortable writing a program (or a set of programs, each doing the assessment slightly differently) to sum up the numbers and compare the result.
While longer and larger the proof in TFA is not really any different.
Re: (Score:2)
While longer and larger the proof in TFA is not really any different... (to the proof I suggested)
I think I disagree with you there. They claim to have found a limit on (the solution space of) a conjecture. This proof (has to) is to prove that this limit is correct. A far different beast, as the patterns arising from / within the number line are completely different in the two cases
Re: (Score:1)
Sure, but if you tell me you've proven that the first million digits of pi don't repeat and you generated them with a computer, I can at least do some basic checks:
1) There are a million digits.
2) They don't repeat.
3) To the limit of the resources available to me I can run my own pi generation routine and ensure that my output matches yours.
That's how I was thinking about this proof, but I do realise it's different. Handling 200TB of boolean logic operations is kind of funky!! :)
Re: (Score:2)
This is more extreme in that nobody can reasonably go over that much proof, no matter how dedicated they are, but in principle it could be done by overlapping teams of people. It won't be, because people don't doubt it sufficiently. Various people will look at various parts of the proof. But it *could* be done.
This has to be seen as a problem. I'm not a mathematician, but I do have a Master's in CS, and I can pretty much guarantee you that program they ran to generate this proof has a bug in it. It may not be a bug that affects the proof, but *all* programs of any appreciable size have bugs in them. ALL.
Re: (Score:3)
What you need to realize is that proofs by humans will also have "bugs". This is why it's important to have multiple independent proofs, if possible, and failing that to have multiple reviewers. But multiple reviewers have been known to overlook the same mistake.
Mathematicians hate the concept, but the foundations of math are not secure. They depend on what humans find convincing evidence. To an extent reproducing the proofs via computer strengthens the proofs, as that reduces the inherent bias. (Every
Re: (Score:2)
Re: (Score:2)
That's what proof has always meant. It's never meant absolute certainty...except that people want to think that that's what it means. (This is one of the inherent biases that is shared by [almost?] all people.)
The think that's changed about the nature of proof in the last 2000 years is that people are more willing to accept that there may be blind spots in their thinking. I attribute this to a combination of more people living in cities, and fast communication across distances. People today get exposed
Re: (Score:2)
That's what proof has always meant. It's never meant absolute certainty
That's what I was taught it meant. A lot of proofs build on other proofs. If the first one turns out to be "buggy", then you'd have to re-evaluate every single later proof that used it too. That could get to be a nightmare.
Thinking back on it though, the teacher I had for the (Geometry) class in HS that first taught me proofs was the worst math teacher I ever had, bar none (he was a coach, so this was his "beard" class). So I guess I shouldn't be surprised at the idea that he was teaching that wrong...
Re: (Score:2)
Sorry. That's what high school teachers teach you math proof means. And they don't notice the inherent contradiction when they find errors in the proofs that you hand in...but it's there, and blatant when you stop to think about it. More experienced people will make fewer errors, but people aren't infallible. That's reserved for the Pope, and even there only on matters of (current?) doctrine.
Re: (Score:3)
Why would you expect the code for this program to be of such a size that the human mind couldn't grasp and verify
Colloquially, if its bigger than "Hello World", it has bugs. Lots of "Hello World"s have bugs too.
But if you are talking about Formal Verification, that's actually a research topic in CS. Its possible to do, but very expensive. Usually you have to use special compilers designed for that, like SPARK [wikipedia.org]. You ever heard of anyone using SPARK? Well, that should tell you how common that is.
But even then, that doesn't mean you don't have bugs. As Math/CS god Donald Knuth [stanford.edu] once said of a relatively more simple queui
Re: (Score:2)
But if you are talking about Formal Verification, that's actually a research topic in CS. Its possible to do, but very expensive. Usually you have to use special compilers designed for that, like SPARK [wikipedia.org].
I was wondering why you'd need "special compilers" for this...and it turns your it's actually some kind of augmented Ada. Well, obviously, if you start with "traditional" source code, a lot of the information is already lost! One wonders if it isn't simply better to start with some kind of a correct high-level specification and then to translate it down to machine code with a series of transformations (some of them potentially custom) that provably preserve the invariants of the original code between any tw
Randall Holmes on the consistency of Quine’s (Score:1)
Do you mean Randall Holmes on the consistency of Quine’s set theory, New Foundations? https://arxiv.org/abs/1503.014... [arxiv.org] (see also http://www.logicmatters.net/20... [logicmatters.net])
Re: (Score:2)
IIRC, the paper I was talking about was by someone from Japan, so probably not that one. If not, I'm not really surprised that there's more than one. (OTOH, he says an earlier version of that proof had been checked by a group of mathematicians, so unless that happened since I heard about it, it's definitely another proof.)
Unfortunately (in this case) I'm a programmer, not a Number Theory mathematician, so the details of what the proof was about, even in general terms, didn't stick in my memory.
Re: (Score:1)
"that is unreadable unless you know enough maths to not need to look it up."
And if you're looking it up on Wikipedia then you'll be caught in a never-ending loop of inadequate comprehension... :)
Re: (Score:2)
Re: (Score:2)
I'm not sure why "uses a computer" necessitates a new class. It seems to me that your argument applies to proof by exhaustion whether done by hand or computer. Also it is not unheard of to try to reach simpler proofs after constructing a complex one - the investigation doesn't have to stop here, but now we know the answer.
Re: (Score:2)
Well, it's a continuum. Dividing a problem into a trillion cases and dividing them into two might be the same in principle, but not in practice.
Dividing something into countably infinite cases probably counts as even more of an "insight-based" proof, because then carrying out the proof by induction requires organizing those cases in some way that makes your argument convenient.
Re: (Score:2)
How is a machine 'computed' proof any different from a human 'computed' proof?
Re:Yes. (Score:5, Insightful)
It's proof, but the problem is the measure of "largest math proof ever" is dumb. I could let a computer (or preferably a cluster) generate proof that every natural number below 200 trillion is followed by another, and there are no gaps, and it would easily trump that as the "largest math proof ever". What's that you say, it's not the simplest proof? True, but my algorithm just didn't hit on the simplest proof yet... Or if you prefer, I can generate proof of the exact number of primes below 200 trillion, it would beat that record by far and as far as currently known, have no simpler proof. For that matter, the Great Internet Mersenne Prime Search is constantly generating proofs that, if written and dumped out sequentially, would beat the pants off this record. But I hope we're not (or shouldn't be) merely competing for "the largest waste of computing power ever" :)
Re: (Score:2)
Also.... Let's say you just wanted to publish a really long proof, but it turned out what you wanted to prove wasn't true after all....... So you conveniently stripped out the one counterexample you found from the data.
How the hell is a human going to discover that you cheated, or that your proof is wrong because of a rounding error in your program?
With a normal proof your reviewers don't need to go through extreme measures to be able to verify your result.
Re: (Score:2)
Re: Yes. (Score:2)
Re: (Score:1)
I wonder what the power bill was for the proof.
Re:Yes. (Score:4, Informative)
Re: Yes. (Score:1)
Well, that proof at least is less than a terabyte!
Re: (Score:1)
Came here to say the same thing. The nice thing about a compact proof is that it may generalize to other situations or offer greater insights. This is certainly not a compact proof. But, to say it's not a proof is ludicrous. It's a very explicit and detailed proof.
It's the difference between adding up the numbers 1 through 100 sequentially (perhaps by counting on your fingers even), and using Gauss' insight to take a short cut. [wbilljohnson.com] The computer didn't take any insight-yielding shortcuts, but still got the
Re: (Score:3)
Of course it's a proof.
Not so fast. There are several [umd.edu] mathematicians [arxiv.org] that don't necessarily agree [google.lv] with that statement. At least not in its strongest form. (We'll ignore the editor basing their argument on the wrong thing, of course being "satisfying" to a human has little bearing on the "proofness" of a mathematical argument).
In fact, whether computer generated proofs that are too large to check by human mathematicians are really proofs at all is a question that's alive (if not exactly well) in the mathematical community, and you
Re: (Score:3)
So what's the difference? In the
Re: (Score:2)
Yes. Don't take my argument to mean that I want to throw out the baby with the bathwater. I'm a firm believer in the use of computers in mathematics. I think we're only just scraping the surface of what's possible. (To add to your example: there's interesting work in statistics for example, where Monte Carlo type simulations have demonstrated that certain statistical tests are much more accurate and valuable, compared to others, on a wide range of different data. Results that were very difficult, if not imp
Re: (Score:2)
Yes, I (and many others) argue that something does change, when proofs become so large that other human mathematicians can't check them.
The social process of mathematics is meant to adress the first kind of problem, i.e. determine that some proofs are incorrect. That's why they're written up and published they way they are. So that others can follow them and make their own judgement as to whether they're true or not. Only when we have a broad consensus from peers do we update our text books and pronounce so
Re: (Score:2)
Very disappointing. (Score:2)
I really wanted the answer to be 42.
Re: (Score:1)
I really wanted the answer to be 42.
They never finished the work: If you add all the digits in 7824 you get 21; the multiply by 2 (the number to which A, B, and c are raised), you get 42! Any real galactic hitchhiker can see this!
Proof? (Score:3)
This doesn't sound like a proof to me. It sound like they disproved the hypothesis at 7,825. It's kind of like saying that they proved that there are no strings of 8 consecutive zeros in the decimal representation of pi. Well, until you get up to about 172,000,000 digits, at which point there is one.
Re:Proof? (Score:5, Informative)
They proved that in every partition of the positive integers into two classes, one class contains a solution to the equation $a^2+b^2 = c^2$. The method of proof is by showing this is already two for any partition of the interval {1,2,...,7,825} into two classes.
This is not entirely surprising; probably there will eventually be quantitative bounds showing that if you colour the integers in {1,2,...,N} in two colours then there are at least f(N) monochromatic Pythagorean triples for some increasing function f(N). Then 7,825 is the first N where f(N)>0, that's all.
I do agree with you that Graham probably expected a proof of the quantitative type rather than a computer search, because many other Ramsey theory problems have quantitative solutions, but there's nothing wrong with starting with a computer search.
Re: (Score:1)
Re: (Score:2)
Agreed. I am curious if it could have been much smaller, perhaps a single page, to show just the set of values that failed the test, or was that what took 200 TB? Sounds like you'd need to show that all 7825 integers had been shown to have been cycled through all possible color combinations, but were all those combinations tabulated to be the 200 TB of data?
Re: (Score:3)
Isn't it more like they *disproved* the hypothesis that "there are no strings of 8 consecutive zeros in pi" by finding an example at a given place?
As a non-mathematician - do I understand this correctly?
Expressing a proof that partitioning is possible for {1,2,...n} is simpler - you just provide an example. The hard part is proving that no such partition exists for a given n.
In this case, they both proved the specific cases up to 7,824, and disproved the general case by proving it impossible for the specif
Science vs Maths. (Score:2)
Isn't it more like they *disproved* the hypothesis....[snip]....As a non-mathematician - do I understand this correctly?
Yes and no, terms such as "proof" are often used in a casual way. Science doesn't offer proof or truth, it offers evidence. Maths doesn't have hypotheses, it has conjectures and truth. This is because Maths is an axiomatic system, the universe is not an axiomatic system therefore Science doesn't have axioms, it has assumptions. A properly formed mathematical conjecture (or statement) is "proven" by demonstrating it is true or false by the axioms of the system.
Having said that, the conjecture was in inde
Re: (Score:2)
Maths doesn't have hypotheses, it has conjectures and truth. This is because Maths is an axiomatic system
The axioms are the hypothesis. Change them and you get a different mathematics. In that sense, in mathematics everything is hypothetical.
Actually mathematics does have hypotheses. However there are very few, they are called axioms and hardly raise any doubt about their validity, with the possible exception of the axiom of choice.
And Euclid's fifth postulate [wikipedia.org]: change this hypothesis and you get different geometry [wikipedia.org].
There are other issues with axioms:
Do we restrict ourselves to first order predicate logic (like Tarski's Axioms for Euclidean geometry [wikipedia.org]) or do we allow higher order logic (like Hilbert's axioms for Euclidean geometry [wikipedia.org])? Such choices have consequences for completeness and decidability.
THIS belongs on Slashdot (Score:3, Insightful)
On topic, what is the content of this 200tb proof? Is that just a text file where each character is a bit? How many libraries of congress is this proof?
Whatever the content, congrats to this team of mathematicians.
Contents of the 200TB proof (Score:3)
Consider the integers between 1 and 7285. To each integer i assign a boolean variable P_i. These variables encode the partition of these integers into two classes (think of P_i as encoding the statement ""the integer i belongs to the first class").
Now let $a,b,c$ be a Pythagorean triple (a^2+b^2=c^2 and 1
Finally, the claim "every triple is not monochrom
Re:Contents of the 200TB proof (Score:5, Insightful)
Re: (Score:3)
You can use less than and greater than signs if you HTML-escape them, eg: "<" (<) and ">" (>).
Re: (Score:2, Insightful)
This is absolutely news for nerds.
I'm going to play devil's advocate and point out that this story literally boils down to "someone used a computer to do what computers do."
Re: (Score:1)
"Most of the time computers are used to shitpost on forums and look at porn/cat videos."
OR do all three at once!!! SHIT POST [imdb.com]!!!! :)
Of course it's a proof! (Score:2)
It's just that it's an experimental proof instead of a purely mathematical one.
And it's hardly the first time this has been done - the 4 color math problem was proved by computation back in 1976.
Computer-assisted proofs are proofs (Score:3)
Well, part of the argument is proving that (if implemented correctly) the algorithm actually solves the problem. But in fact this part is redundant -- because what the computer does is actually write out a proof of the theorem.
The point is that while coming up with a proof takes work or ingenuity, verifying the correctness of an proposed proof (written in sufficient detail) is purely mechanical. In other words, you don't need to believe or check anything the researchers have done. You simply need to take the output of their program and use a proof-checker to verify that this output is a valid proof.
For many combinatorial theorems this is the way of the future, and while the submitted may be unsatisfied by a proof which doesn't provide intuition, isn't that better than no proof at all?
Re: (Score:3)
Also, consider simple proofs by induction. Besides the actual induction, you need to show that a trivial case works, which is usually plain arithmetic that could be done on a computer. More complicated proofs may require multiple brute-force cases before the actual math can be done. For example, I recall a proof of Bertrand's postulate which first needs individual cases for n < 2000.
It's a bit like physics where you need some concrete system of measurements, a real-world grounding for your abstract wo
Writing this out by hand would have been a b*tch (Score:2)
Retarded question ... (Score:2)
Is the proof really a proof if it does not answer why there is a cut-off point at 7,825, or even why the first stretch is possible? Does it really exist?
When you have counted all possible outcomes and put a note for each one into a basket, collecting all notes of the same kind, then the result is a proof.
What else should it be? There is no "why" needed.
The "why" would be interesting as it might lead to a formula where you just put in a few parameters and get a "colour" as answer.
The easiest proof btw is the
Limits (Score:2)
Why not ask this guy? [youtube.com]
Clobbering With Statistics (Score:1)
It's just "Clobbering With Statistics" which is fun, and probably easier to get funding for, as you just buy a bunch of equipment.
One question: (Score:2)
Re: (Score:2)
QED (Score:2)
If the file ends with "QED", then but definition it is a proof.
Re: (Score:2)
If the file ends with "QED", then b[y] definition it is a proof.
Except of course if it is a text about Quantum Electro-Dynamics.
entire [N]/y (Score:1)
Proof of cutoff point (Score:1)
One could image the editors being just a little bit 'happier' with the proof if just a bit more information was provided about the number 7825.
Correct me if I'm wrong, but 7825 has to be part of at least one Pythagorean Triple, no? If you take all the integers up to 7824 and you can divide them up, but then you fail when you add 7825, then 7825 has to be part of a triple, otherwise it wouldn't be a tipping point.
So there has to be at least one set of numbers a and b such that a + b = 7825. a and b must be s
The proof program (Score:1)
# natural numbers into to sets so that
# _all_ pythagorean tripples are split up,
# having some elements in one partition and
# some in the other.
#
# The math proof relies on this being true for all triples
# of numbers up to N = 7285, something which can be tested by
# a computer.
#
# We create a logic expression that is true iff
# there exists some partition such that all triples
# are split, and false otherwise. The computer
# checks that this is indeed al
Re: (Score:1)
range(1,N+1)
simple proof (Score:2)
Is this really a proof? (Score:1)
Is this really a proof? I was always taught that a proof shows that the argument presented is always true -- not just for the first 7,824 times as is the case here, but always (obviously given the axioms used).
For instance, in Euclidean geometry, one can prove that the sum of the angles of a triangle are two 90 degree angles or 180 degrees. They don't total to 180 degrees up to some finite point as in the article.
Don't get me wrong. There was impressive work done here. It just doesn't amount to a proof, un
What would Ramanujan Do? (Score:3)
Do?
He will simply calculate all possible Pythagorean triples in his head, write down 7285 in a piece of paper as the "solution" and leave the proof as an elementary exercise to the reader.
Cumulative Rounding Error (Score:2)
That's all I got.