Slashdot Mirror
Computer Generates Largest Math Proof Ever At 200TB of Data (phys.org)
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?
Of course it's a proof. Who taught you what the word "proof" means? Perhaps you were looking for "satisfying answer," dear editor?
Bio questions? Ask me to start a Q&A journal. Computer analogies available for most topics!
I really wanted the answer to be 42.
Is it just my observation, or are there way too many stupid people in the world?
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.
Ask me how the Heisenberg Principle may or may not have saved my life.
This is absolutely news for nerds. Please post stories like this one and fewer "Why Trump/Clinton are lizard people" stories.
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.
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.
A thousand pounds of wood moving at 300 feet per minute. Don't get in the way.
Good proofs serve two purposes. Obviously they provide a yes/no answer to a question, but equally importantly they teach us things about the problem and the underlying structure of mathematics. This serves the first purpose but fails on the second.
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?
Brings back memories of hand writing proofs in Adv Calc and Analytical Calc, getting 6 pages in and finding a mistake. 199.99999 TB written by hand and finding a mistake = bad year :-)
Ah, I feel much better now.
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 proof by counter example ... met already plenty of Ph.D's who did not grasp that concept.
"All (chicken) eggs are white!"
"No, look, here I have a brown one!"
"That proofs nothing!"
Wow ...
Cost free eBook I read (by iBook/Kobo/Amazon/ObookO/Gutenberg etc.): "The Green Odyssey" by Philip Jose Farmer.
"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"
if you have 2 colors, and 3 numbers, and you have to label the 3 numbers with a color, but no 2 numbers can have the same color, then you need 3 colors.
they choose to describe the problem in worst way
someone has to peer review it
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 monochromatic" is obtained by taking the conjuction of the Q_{a,b,c} over all triples (a,b,c) as above. It's a huge boolean expression and the goal is to show that it always evaluates to FALSE (in other words, that for any boolean assignment to all the P_i), the huge conjugation always takes the values.
The proof works by manipulating this boolean expression: it has 200TB of instructions on how to manipulate this huge boolean expressions step-by-step in ways that obviously don't change its truth value, so that at the end one of the clauses in the conjunction simply reads "FALSE", making the whole expression indeed universally false. A computer program discovered this list of manipulations, and a separate (much simpler) program can easily verify that the manipulations are of the right kind (they don't change the truth value) and that at the end of the manipulation you get a clause saying FALSE.
Why not ask this guy?
A proof is a proof. What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven.
-- Jean Chretien (former prime minister of Canada)
Has been working on this since 1984. It just spit out '9'. I probably should have optimized the code a little more.
All this ranting against computer proofs by "real" mathematicians reminds me of the economics example of the buggy whip manufacturers. They were very vocal about being put out of business by the new-fangled machines, too.
It's just "Clobbering With Statistics" which is fun, and probably easier to get funding for, as you just buy a bunch of equipment.
.. as winning a fight in junior high school by bringing your big brother in to clock the guy.
Better not mess with me! Because, uh...
Has anyone checked all 200TB of data? Are you certain that there is no flaw in the output?
linquendum tondere
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 indeed "disproven" by the discovery of a counter example.
And did you exchange a walk on part in the war for a lead role in a cage? - Pink Floyd.
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).
So it says it is not entire?
If the file ends with "QED", then but definition it is a proof.
So it says it is not entire? [Y]/n
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 smaller than 7825 which is why 7825 has to be the c in the Pythagorean theorem.
So if any such numbers a and b could be given as additional information, the reason for 7825 would be clearer.
Like if you're dividing red and blue marbles over 2 containers and you can't have two of the same color in a container. You can divide 4 of them, 1 of each color in each container, but when you try to place a fifth, all containers are full.
Here, same thing: when you reach 7825, all the containers are full and you can't squeeze in an extra triple anywhere.
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.
I wonder how much of those 48 hours were spent on string manipulation. echo '200000/(2*24*3600)' | bc -l # == 1.2
# Claim: It is not possible to make a partition of the
# 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 always false (=unsatisfiable)
# for all possible partitions.
#
# Below P13 means that integer 13 belongs to the first set
# and ~P13 means that it belongs to the other set, etc.
from sympy import *
N = 10 # should be 7285
def is_a_triple(a,b,c): return a**2+b**2==c**2
tripplesUpToN=[(a,b,c) for a in range(N) for b in range(N) for c in range(N) if is_a_triple(a,b,c)]
def notAllInSamePartition(a,b,c):
Pa,Pb,Pc=var("P{} P{} P{}".format(a,b,c)) # Create variables P13, P57, etc.
return ~( (Pa & Pb & Pc) | (~Pa & ~Pb & ~Pc) )
# Expr = All triples of numbers up uo N are split up over different partitions
Expr = And(*[notAllInSamePartition(a,b,c) for a,b,c in tripplesUpToN])
# Expr is unsatisfiable, because always some triple will be completely in one of the partitions, so it should print False
print satisfiable(Expr)
Shit's brown.
It feels like we have really reached the end of pure math as an interesting research area now.
Since Godel et al we know that searching for proofs given axioms is a mechanisable though sometimes non-terminating grind, pretty similar to searching for the next biggest prime number. We know there are an infinite number of theorems out there of which some can be ground out by search.
So what's the point of having human pure mathematicians any more? The act of searching for proofs is no longer interesting in itself, apart from maybe as one example of a cognitive heuristic process for the psychologists to study. Should we just declare pure maths, like theoretical chemistry, to be completed and "over", and spend research funds on something else now ?
I've got a simple proof of this but it's slightly too large for this comment box. I'll post it laterrrrrrrrrrrrr...
sag
I think there are more important things to be working on.
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, unless that is now a subjective term.
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.
sed -e 's/Chuck Norris/Rajnikant/g' joke > fact
We already went through this in the 1980s. The four color theorem - the idea that you can draw any map using just 4 colors and no neighboring regions with shared edges will have the same color - resolves down to 1476 possible simplified map configurations. Appel and Haken wrote a computer program to check each of those configurations, and none were found to violate the theorem. Thus the theorem must be true.
Mathematicians initially rejected the idea that this constituted a mathematical proof for the reasons that have been posted in the comments here. But in the 1980s they came around and begrudgingly accepted that the theorem had in fact been proven, thus legitimizing computer proofs by exhaustion of the solution space. It's really no different than proof by reduction, where you can reduce a problem down to just one or two cases, and simply show that those one or two cases don't violate the theorem being proven.
Do you mean Randall Holmes on the consistency of Quine’s set theory, New Foundations? https://arxiv.org/abs/1503.014... (see also http://www.logicmatters.net/20...)
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.
I think we've pushed this "anyone can grow up to be president" thing too far.
Bunch of nerdies
That's all I got.
Political debates have me rolling my eyes so much I think I got optical whiplash. I should sue. - Foamy The Squirrel