200 terabyte proof demonstrates the potential of brute force math

https://motherboard.vice.com/en_us/article/padnvm/200-terabyte-proof-demonstrates-the-potential-of-brute-force-math

by sharemywin • 9 years ago

144 144 9 years ago

motherboard.vice.com

Does anyone know what the proof actually proves, and how the reduction was formulated?

curiousgal2• 9 years ago

Theorem — The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.

https://arxiv.org/pdf/1605.00723.pdf

jordigh• 9 years ago

Yeah, when I saw "200 terabytes" I thought it was going to be about the Erdős discrepancy problem, since that's been making the rounds in the popular press, but turns out that only required 13 gigabytes for the 2010 proof.

I'm glad that Terry seems to have found a different proof. I attended a discussion of it during last week's Mathematical Congress of the Americas here in Mtl, and I think they were saying that Terry's proof seems correct.

rocqua2• 9 years ago

Abstract:

-------------------------

Recent progress in automated reasoning and supercomputing gives rise to a new era of brute force. The game changer is “SAT,” a disruptive, brute-reasoning technology in industry and science. We illustrate its strength and potential via the proof of the Boolean Pythagorean Triples Problem, a long-standing open problem in Ramsey Theory. This 200TB proof has been constructed completely automatically—paradoxically, in an ingenious way. We welcome these bold new proofs emerging on the horizon, beyond human understanding— both mathematics and industry need them.

Xeoncross• 9 years ago

This 200TB proof

How do you verify a 200TB proof?

falcolas• 9 years ago

Generate another proof (using a different method; Coq?) of the proof? That's all I can think of.

justinpombrio• 9 years ago

With software.

johncolanduoni2• 9 years ago

Usually by trusting/auditing/verifying the program you use to verify the proof. Which will be much easier to do by hand than 200TB worth of data.

slaymaker19072• 9 years ago

Not only do you need to verify the code, you also need to generate the proof multiple times since there is a significant possibility of hardware error with that large of a dataset.

SilasX2• 9 years ago

Same way as any proof, right? Check that each step is valid; in this case, that the symbol manipulation obeyed the rules.

nickpsecurity3• 9 years ago

With a proof checker. They're usually tiny for easier verification. Some are trying to verify the verifiers. HOL/Light and Jared Davis's Milawa esp come to mind. Milawa's layered approach is pretty neat.

http://www.cs.utexas.edu/users/jared/milawa/Web/

wiz21c• 9 years ago

You prove that your SAT solver is correct. Then you prove that the way you expressed the problem is correct.

I'm not in that SAT stuff enough to know if one can prove that :-)

rrobukef3• 9 years ago

Most SAT solvers work similarly. The authors extended a technique (RUP to DRUP to DRAT) that creates a co-witness for the SAT problem. (This witness is not polynomial in the input size but proportional to the solving time.) The SAT solvers can output this format without slowdown. It is essentially printing some data structures (learned clauses) in the non-hot loop. The rest is clever heuristics, parallelization and work stealing.

The new technique creates smaller and easier witnesses. The solver they used output this witness during solving and saved it. They also created a formally-verified witness verifier. Finally run the verifier for every witness in the sub-problem.

maxxxxx• 9 years ago

I tend to get sceptical when I hear the word "disruptive" to describe something.

danharaj2• 9 years ago

The article: https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...

Note that most people believe that co-NP /= NP, which implies that an unsatisfiability proof via SAT solving in general won't be efficiently verifiable.

maaaats• 9 years ago

Could this be used to prove co-NP = NP, though?

danharaj2• 9 years ago

probably not

opportune5• 9 years ago

From a technical standpoint, this is a terribly written article.

First, giving an example of solving an algebraic equation using brute force is misleading, because you can't enumerate all values of a real number.

Second, the risks of secrutity regarding brute force computing having nothing to do with SAT.

Also, their description of SAT is inaccurate. It's not new, and it was actually one of the first formal problems studied in computer science. Also, the original, linked paper notes that it is not brute-force computing that is itself the breakthrough, but the addition of heuristics in SAT solvers that make brute-forcing feasible.

slaymaker19072• 9 years ago

Even for integral/rational solutions, the problem is still Turing complete since there may be no solution at all.

opportune5• 9 years ago

True, countability doesn't change the problem. Solving a mathematical equation is just a bad way in general to explain what a brute force solver does. Much better to use an example such as a crossword puzzle or sudoku

legulere• 9 years ago

This article is about SMT-solvers, which are used in formal verification, which can be about security. SMT solvers are kind of newish: https://excape.cis.upenn.edu/documents/ClarkBarrettSlides.pd...

opportune5• 9 years ago

The article and the linked paper (https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...) are about SAT solvers. The paper mentions SMTs briefly in passing. There may be a disconnect in whether SMTs are referred to as SAT solvers or their own distinct entity, though

Apologies for being nasty

bassman9000• 9 years ago

I stopped reading after this

This is thanks to a newish technology called Satisfiability (SAT) solving, which is a method of generating proofs in propositional logic.

SAT3 was old when I was in college. And it's not to generate proofs.

chx• 9 years ago

Finally someone notes that! I read "You could take a basic algebra problem as an example: 2x + 100 = 500. To solve this with brute force, we simply check every possible value of x until one works. " and began to twitch.

Havoc• 9 years ago

I suspect the average mathematician won't consider that "elegant".

vernie• 9 years ago

Sure, but so what?

Koshkin4• 9 years ago

It is unlikely that such proof can be considered a contribution to mathematics. Finding "elegant" proofs (and not just "facts"), building conceptual frameworks in the process, is the heart of mathematics as a human activity.

coldtea3• 9 years ago

Well, the average mathematician can't define what they mean by "elegant" either.

bmc7505• 9 years ago

Has there ever been a brute force proof that discovered the existence of a solution previously thought impossible? Something like a new tiling or proof by contradiction that found a positive example?

qubex4• 9 years ago

If I do not remember incorrectly, the proof of the Four Colour Theorem is essentially a brute-force one: a method of generating every possible graph that represents adjacency of tiling polygons on a 2D surface, and a subsequent colouring scheme for each and every one of them that never uses more than the desired four colours.

opportune5• 9 years ago

I think the FCT proof doesn't generate every possible graph in that category (as there are infinitely many of them) but rather enumerates a very large set of compositional planar graphs such that all planar graphs are composed of combinations of subgraphs within the enumerated set

bjl2• 9 years ago

Everyone already strongly suspected that the FCT was true. Nobody was surprised by the result, it just took a computer to prove it.

kmill2• 9 years ago

There is a step in the proof which is brute force. The proof is sort of giving a recursive algorithm for 4-coloring: for certain subgraphs, you simplify it, color the result, and use the coloring to color the original graph. There are 633 cases ("reducible configurations") in the recursion, and the annoying part is checking that all 633 actually work. After Haken and Appel, Gonthier wrote a Coq proof http://www.ams.org/notices/200811/tx081101382p.pdf

Sometimes I imagine that if we had much larger short term memories, an argument with only 633 cases would be obvious.

netsec_burn• 9 years ago

I tried bruteforcing the prime equation using known mathematical functions concatenated in different ways with arbitrary constants converging on the distribution of primes. What's pretty cool is I got close to some academic research the produced the 'closest equation for prime approximation', which was a bunch of logarithms in a fraction. Really fun and worthwhile to play around with for problems thought to be impossible.

kirrent• 9 years ago

Probably not what you were thinking of, but the counterexamples to Euler's sum of powers conjecture springs to mind. Despite being around for centuries, it took the use of a computer to find a counterexample.

https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...

the6threplicant• 9 years ago

There has been a lot of examples generated by computer proving conjectures of their existence, I think a people now call this experimental mathematics. For instance in finite geometries, construction of new generalized quadrangles, flocks etc.

janci• 9 years ago

I hesitated before clicking on that link as for a second I thought it would start downloading that 200 TB proof.

munificent• 9 years ago

I really wish I'd known there would be an illustration of a naked woman in an advertisement on the right before I opened this at work.

sheepdestroyer• 9 years ago

Did not see it, shouldn't you use an adblocker at work for obvious reasons?

sharemywin• 9 years ago

sorry didn't see that. ad blind-ness.

Koshkin4• 9 years ago

Sure, "proof mining" is feasible, but the goal of proving a theorem is only rarely finding any proof, it is rather finding a proof that makes sense, is "elegant", and in the best case scenario a proof that actually forms a sensible new theoretical framework in which the theorem becomes almost trivial to prove.

ISL• 9 years ago

If something can be proven by any method, that means that it is true. An elegant proof is often more illuminating, but it isn't precluded by a direct method.

If the proven theorem is useful, isn't it better to be able to make use of it earlier, rather than wait for the elegant proof?

An example: If the AdS/CFT conjecture is demonstrably proven, it will elevate it from "useful computational technique" to "law of mathematics, probably how nature does it, too". I'll take any proof, as early as I can get it, in order to guide our experimental work.

eric_h• 9 years ago

https://en.wikipedia.org/wiki/AdS/CFT_correspondence

In case anyone else had no idea what the parent was talking about.

raattgift• 9 years ago

If the AdS/CFT conjecture is demonstrably proven, it will elevate it from "useful computational technique" to "law of mathematics, probably how nature does it, too".

Gauge/gravity duality under particular circumstances is certainly interesting, but unfortunately our universe is not AdS and in particular does not have a boundary on which the conformal field theory can be constrained. So being able to define string theory nonperturbatively on a Minkowski space defined on the boundary of spacetime is certainly interesting, but as far as we can tell our spacetime does not have that boundary and moreover it would be much nicer if we had a background independent formulation for a nonperturbative string theory, and the gauge/gravity duality does not really offer that. One might draw the analogy to being able to define a patch of Minkowski space around a point on a geodesic through a general curved spacetime: General Relativity explicitly promises only that a smooth coordinatization (e.g. Fermi coordinates) is possible in an infinitesimal neighbourhood around the point although in weak gravity the patch can be much bigger (and the system of coordinates more "Cartesian"). The worry (by this analogy) should be that gauge/gravity correspondence falls apart in strong gravity.

Moreover, it is an enormous stretch to argue that if a large class of bulk theories have the same symmetries as certain boundary theories (or are related in some other way) then therefore there background independent physics are recovered. Rovelli enjoys pointing out that in GR you can always select a preferred frame and map an SR theory over that and do useful computations, but that doing so gives no insights into proper Lorentz-invariant physics, so how does choosing a preferred spacetime and mapping a field theory over that providing insights into quantum gravity?

However, some string theorists (notably Verlinde recently) have been trying to get out of the AdS "box" and think about other chosen spacetimes (e.g. asymptotic de Sitter) to see if some gauge/gravity ideas are even workable for those spacetimes. Maybe they are.

I'll take any proof, as early as I can get it, in order to guide our experimental work.

If you assume -- because General Relativity survives all observational tests and is expected to be completely correct in weak gravity -- that the string theory has to reduce to (or at least fully reproduce) classical GR in the appropriate limit then you can't expect any experiments which could distinguish between the two in the near future. But if you have a string theory that departs from GR in a testable limit, then sure, compare that with existing and future evidence.

However, string theory might testable outside the gravitational sector if the bulk-boundary correspondence covers more than that sector. Given that string theory tends to come with infinite fields, extra dimensions, supersymmetry and other theoretical objects that are not in the Standard Model, then BTSM experiments may have something to say about such string theory models.

noobermin2• 9 years ago

But people often write papers anyway assuming X and Y and Z are true just to see what happens because of it, it's not like you really need it to be true to at least publish things.

And for your example that touches on applications of math, it approaches scientific research from the wrong perspective. If some math follows reality, (agrees with experiment and even better makes predictions that turn out to be right), there is has to be some backing to it, even if the rigor isn't fully there. Physics often runs with ideas before Math has caught up (see QM in the early days, HEP in general, etc).

So, if we back off from applications who, quite frankly, only care about whether X is true in only a few, really important number of conjectures I can think of--big questions like P=NP for example--then math itself I imagine is, well, a study for its own sake. So, what above exhaustive proofs of your run-of-the-mill conjecture? Who would want to read a paper from a math person that merely iterates through a 200TB cache of data?

People forget that science is a social phenomenon as much as it is systematic process.

roywiggins• 9 years ago

If you just care about the correctness of some algorithm, proving it is just tedium and not likely to produce a proof useful for reading anyway. So an exceptionally long, boring proof of correctness generated by a supercomputer is perfectly fine.

nickpsecurity3• 9 years ago

This sort of thing is standard in Frama-C and SPARK Ada for proving code to be safe from common vulnerabilities or crashes. I don't care what the proof terms look like: just that the code won't get hacked. Same with CompCert even though it's meant to be readable. I just want a correct compilation.

Lots of situations where the result obtained is only thing that matters to most users.

raverbashing• 9 years ago

Not really

A proof that works is the most important part. After that you can make it nice

Koshkin4• 9 years ago

you can make it nice

Not the 200 terabyte one, you can't.

hinkley• 9 years ago

It never occurred to me until just now that one of the AI overlord scenarios, and also quite possibly the most plausible one, is one in which AI just exploits some impenetrable proofs to win at economics via information asymmetry. Rather than rounding us up or exterminating us, we just become the live at home kid always begging for money, grumbling about a curfew and having to do chores at 25.

pmiller2• 9 years ago

I would say elegance is often only a beneficial side effect of finding a good proof. A good proof is one that has explanatory value, and gets to the root of why the statement is true.

dgfgfdagasdfgfa2• 9 years ago

Err—presumably the proof that makes sense is a correct proof. How is that not a binary quality?

aschampion2• 9 years ago

It means the proof is explanatory, i.e., that it provides a framework of thought that extends our capability to reason about related problems within our very limited cognitive envelope. Pure proofs, like purely predictive models in science, often do not provide this.

Florin_Andrei3• 9 years ago

When proofs are creeping slowly into the petabyte or exabyte territory, at some point you will not be able to distinguish them from the complexity of Mother Nature herself.

Proof used to be a distillation of a complex phenomenon, or a complex logical tangle, into a smooth thread that one could follow and agree that, yes, this is obvious when you put it this way.

Sure, at some point computers will take over the work of doing proofs, just like in a different trade hammers took over fists, or wheels took over feet, or engines took over muscles, hearts and lungs. But at that point we will have to re-examine this concept of "proof".

fmap• 9 years ago

Many "open problems" in mathematics are not actually that interesting on their own. Take the Collatz conjecture: it's pretty much just the statement that a certain 3 line program terminates. In many cases such as this, it is not the truth or falsity of a statement that interests people, it is the method to arrive at a proof which yields new insights.

For example, the graph minor theorem states that a certain order on graphs does not have an infinite antichain. Classically this may have some interesting consequences, but in reality it's not very useful. However, the proof contains some real gems, such as the notion of tree decompositions and the graph structure theorem that lead to mountains of new results all throughout graph theory and related disciplines. Tellingly, the graph minor theorem is a short and simple question while the graph structure theorem is a deeply technical statement that would not have been conjectured on its own but rather was discovered in the process of showing the graph minor theorem.

hellbanner3• 9 years ago

Start now and make your altcoin, seriously :)

c3534l• 9 years ago

That's one goal of proving a theorem. It's still useful to know the answer ahead of time if you're going to prove it. And some stuff is useful to know anyway. Proving P = NP would be super important to know, even if no one actually understood why. In fact, there's countless theorems that depend on results which have not been proven yet. People may have been doing important work that relies on the Riemann Hypothesis because they incorrectly believed it was true and that time might have been wasted. Additionally, once you find a proof through exhaustive search, it's entirely possible that human beings can go in there and simplify it to a level that can be understood by people. And maybe multiple results might paint a picture that shows us a direction to go in that we wouldn't have guessed beforehand.

awkwarddaturtle• 9 years ago

but the goal of proving a theorem is only rarely finding any proof

No. The goal of proving a theorem is proving it any way possible. And "inelegant" proof is just as much a proof as an "elegant" proof.

and in the best case scenario a proof that actually forms a sensible new theoretical framework in which the theorem becomes almost trivial to prove.

What?

gizmo686• 9 years ago

> and in the best case scenario a proof that actually forms a sensible new theoretical framework in which the theorem becomes almost trivial to prove.
What?

The idea is that, in creating the proof a mathematician invents a new way of looking at the problem. When viewed in this new way, the problem itself sometimes becomes trivial. When this happens, the the framework that was developed could be used to attack new problems that had previously been unapproachable.

joe_the_user• 9 years ago

As others have noted, finding the truth of a theorem is important and elegance has to be secondary in most people's book. Or at least, the truth of a proposition is never not going to be important.

But oppositely, I don't think anyone's demonstrated "proof mining" to be practical in any general sense. Huge proofs have been produced by brute-force, yes, BUT ONLY after the original theorem claim was altered in a clever and important fashion (for 4-color theorem, for Ramsey's theory and so-forth).

pervycreeper4• 9 years ago

Assuming progress continues long enough: as proofs (and theorems) become more complex, the computational difficulty of verification, combined with the inherent physical impossibility of obtaining absolute certainty in the correctness of a computation will transform future mathematics into an empirical science, where mathematical hypotheses will be tested by computer, and results will be considered true only probabilistically.

colordrops6• 9 years ago

That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.

pervycreeper4• 9 years ago

That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.

Not what I'm saying. I would suggest that absolute certainty is impossible wrt verifying conventionally proved theorems as well.

lisa_henderson• 9 years ago

pervycreeper is making the point that all computers are, for practical purposes, probabilistic, since you can never know if a given result is because of a machine failure. In the normal sense of a math proof, one can not "exhaust the problem space" using a computer. Using a computer remains an empirical approach, since there is always the chance that the computer is malfunctioning.

hellbanner3• 9 years ago

What did it prove?

curiousgal2• 9 years ago

Theorem — The set {1, . . . , 7824} can be partitioned into two parts, such that no part contains a Pythagorean triple, while this is impossible for {1, . . . , 7825}.

hellbanner3• 9 years ago

Wow, interesting. Is the 200 terabyte proof necessary for that -- could it be refactored into something smaller?

pcmaffey• 9 years ago

I can't wait for the day when a proof is 'discovered' that no one can comprehend.

krallja• 9 years ago

A 200TB proof is already incomprehensible to humans.

The average reading speed is 200wpm. The average human lifespan is 79 years, or about 41.5 million minutes. If you did nothing but read at 200wpm for your entire life, you might read 8.30 billion words. A word is 5.1 letters, on average, and in ASCII, a letter is one byte. Multiply that all together to get an estimated human reading speed of 42.4 GB/lifetime.

It would take 4728 entire human lifetimes to read this proof once.

This is vastly underestimating the actual number, due to silly things like "eating", "sleeping", "learning to read", etc.

coldtea3• 9 years ago

A 200TB proof is already incomprehensible to humans.

Not really, since what matters is the compressibility of the proof, not its size.

We might not be able to read all individual clauses, but it's enough that we know how the clauses are constructed.

grondilu3• 9 years ago

You could take a basic algebra problem as an example: 2x + 100 = 500. To solve this with brute force, we simply check every possible value of x until one works. We know, however, that it is far more efficient to rearrange the given equation using algebraic rules and in just two computations we get an answer.

I gave some thoughts about this lately, and it occurred to me that it's a problem that is similar to how computers play chess. I'd like to know if I'm right.

The equation 2x + 100 = 500 is an algebraic identity and with algebraic rules there is a finite number of ways to transform it. For instance, x + x + 100 = 500, 3x - x = 400, x + 200 = 600 - x, and so on. Each of these new equations can once again be transformed in a finite number of ways. So basically the initial equation is the root node of a tree that represents all the ways the equation can be transformed.

So it's a similar problem than for chess, or many other board games, where you start from a position and you must explore a tree of possibilities to find the leaves (checkmates, for instance). For an equation the leaves are nodes of the form x = numeric value.

Does that mean success in solving board games can have applications in computational math?

nawgszy• 9 years ago

Sorry, this is just a trivial observation, but if you're going to accept

x + x + 100 = 500

and

3x - x = 400

you can probably list any variety along the lines of

(n)x - (n - 2)x + y = 400 + y

so clearly that isn't a finite transformation space.

Now, these transformations might look trivial, but this problem is too. So there's an interesting question of bounding your algebraic transformations to a subset of all possible transformations that still make all possible solutions available, which ultimately doesn't answer yours.

grondilu3• 9 years ago

True, it is not finite. Still, considering the algorithm will not attempt to search the tree exhaustively anyway, maybe the fact that the tree is infinite does not make much difference.

PS. On second thought the number of rules is finite, so the number of possibilities has to be finite, at least if you apply the rules one at a time. It's the iteration of the rules that makes the tree infinite.

joshjje• 9 years ago

The fact that you are transforming a constant, into other constants, should be clear there is an infinite way to transform that. And so on. Also it is not similar in chess in that those equations that you derive from the starting one, are easily simplified back to the original one (or close to it).

grondilu3• 9 years ago

I poorly chose my examples. There is a finite number of rules so for each step there is a finite number of possibilities.

For integers for instance, the rule is in their definition, and there is only one. 2 is 1+1, 5 is 4+1 and so on.

are easily simplified back to the original one (or close to it).

Not really. The counter-example being expansion of factors.

nshepperd• 9 years ago

Yes, you can treat proof search as a game tree with "proof states" in the nodes and apply game playing heuristics to guide the search, eg. alphago style. From what I've read, these approaches do work, see for instance https://arxiv.org/abs/1701.06972. Nothing spectacular, but it's an improvement.

lotsoflumens2• 9 years ago

It's called Finite Domain Constraint Programming and it's been studied for about 50 years.

GnarfGnarf• 9 years ago

There's an error in the article.

    ((true AND false) OR true) AND NOT (true OR false)

is false, not true as asserted in the article.

cakebrewery• 9 years ago

Maybe he corrected it afterwards but he clearly says it's not.

phasnox• 9 years ago

This one is "from The Book" - P.E.

AstralStorm2• 9 years ago

A proof being valid does not mean the theory is useful or valid. If SAT was used, it means it is internally consistent in first order logic assuming the solver did not have a bug in it. (I bet the program was also verified.)

You can simplify these proofs by extracting subproofs and replacing them from database by substitution. It is like compression but makes more sense.

Radim• 9 years ago

Mandatory insight-vs-bruteforce-in-science essay:

Peter Norvig, 2011: On Chomsky and the Two Cultures of Statistical Learning

http://norvig.com/chomsky.html

lotsoflumens2• 9 years ago

It's disappointing that the authors use the term "brute force" to describe modern SAT solving, in an article intended for people who may not be familiar with the algorithms used.

That term implies that the speed of the computer that was used to find the solution is the determining factor.

It is not. Modern SAT solvers use very elegant search algorithms that have enabled the solution of SAT-encoded problems that could never have been solved if only "brute force" was used.

200 terabyte proof demonstrates the potential of brute force math

Related Stories