200 terabyte proof demonstrates the potential of brute force math(motherboard.vice.com)
motherboard.vice.com
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
151 comments
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.
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.
> 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?
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?
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.
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.
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.
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.
Nope, a single rule still has an infinite number of possibilities. As an example, multiplying both sides of the equation with an arbitrary constant produces a new valid equation, and there's an infinite number of constants to multiply with. (Bonus point: You get to choose what kind of infinity - countable or uncountable)
The reason a move tree[1] in a chess game has a finite number of nodes is not due to the finite number of possible transforms, but due to the fact that the number of possible board states is finite.
[1] graph, really.
The reason a move tree[1] in a chess game has a finite number of nodes is not due to the finite number of possible transforms, but due to the fact that the number of possible board states is finite.
[1] graph, really.
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.
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).
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.
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.
It's called Finite Domain Constraint Programming and it's been studied for about 50 years.
There's an error in the article.
((true AND false) OR true) AND NOT (true OR false)
Maybe he corrected it afterwards but he clearly says it's not.
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.
You can simplify these proofs by extracting subproofs and replacing them from database by substitution. It is like compression but makes more sense.
What did it prove?
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}.
Wow, interesting. Is the 200 terabyte proof necessary for that -- could it be refactored into something smaller?
This one is "from The Book" - P.E.
[deleted]
Does anyone know what the proof actually proves, and how the reduction was formulated?
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
https://arxiv.org/pdf/1605.00723.pdf
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.
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.
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.
-------------------------
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.
I tend to get sceptical when I hear the word "disruptive" to describe something.
> This 200TB proof
How do you verify a 200TB proof?
How do you verify a 200TB proof?
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/
http://www.cs.utexas.edu/users/jared/milawa/Web/
There is a verified DRAT-trim (the proof checking format used) implementation in Isabelle/HOL [1]. Apparently it is faster than the original:
``We have presented a formally verified tool chain to check DRAT unsatisfiability certificates. In single-threaded mode, our approach is more than two times faster than the (unverified) standard tool drat-trim, on a benchmark suite taken from the 2016 SAT competition.''
[1] Lammich, Peter. "Efficient verified (UN) SAT certificate checking." International Conference on Automated Deduction. Springer, Cham, 2017.
``We have presented a formally verified tool chain to check DRAT unsatisfiability certificates. In single-threaded mode, our approach is more than two times faster than the (unverified) standard tool drat-trim, on a benchmark suite taken from the 2016 SAT competition.''
[1] Lammich, Peter. "Efficient verified (UN) SAT certificate checking." International Conference on Automated Deduction. Springer, Cham, 2017.
Neat. Here's two more on that topic that go further:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.459....
http://matryoshka.gforge.inria.fr/pubs/sat_sister.pdf
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.459....
http://matryoshka.gforge.inria.fr/pubs/sat_sister.pdf
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.
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.
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 :-)
I'm not in that SAT stuff enough to know if one can prove that :-)
Generate another proof (using a different method; Coq?) of the proof? That's all I can think of.
With software.
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.
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.
You should verify the proof multiple times, but there's no reason to generate it multiple times. If there was an error in the witness generation proper verification will catch it, and if there's a problem with the verification regenerating the witness will not help.
Excellent point.
Hardware error is almost certain in this case. c.f. rowhammer or bitsquatting.
Hardware error is almost certain in this case. c.f. rowhammer or bitsquatting.
I think it would be pretty unlikely to trigger rowhammer accidentally. The incidence of random (memory) errors is very low. Something like once every 1.5 years...
This study from Google is pretty interesting:
http://www.cs.toronto.edu/~bianca/papers/sigmetrics09.pdf
This study from Google is pretty interesting:
http://www.cs.toronto.edu/~bianca/papers/sigmetrics09.pdf
I compared to rowhammer and bitsquatting.
From the paper that you cited:
Our first observation is that memory errors are not rare events. About a third of all machines in the fleet experience at least one memory error per year (see column CE Incid. %) and the average number of correctable errors per year is over 22,000. These numbers vary across platforms, with some platforms (e.g. Platform A and B) seeing nearly 50% of their machines affected by correctable errors, while in others only 12–27% are affected. The median number of errors per year for those machines that experience at least one error ranges from 25 to 611.
From the paper that you cited:
Our first observation is that memory errors are not rare events. About a third of all machines in the fleet experience at least one memory error per year (see column CE Incid. %) and the average number of correctable errors per year is over 22,000. These numbers vary across platforms, with some platforms (e.g. Platform A and B) seeing nearly 50% of their machines affected by correctable errors, while in others only 12–27% are affected. The median number of errors per year for those machines that experience at least one error ranges from 25 to 611.
You have hecksums and other internal consistency checks to deal with those.
They won't actually help. With hecksums, you're darned if you do, and darned if you don't.
;-)
;-)
Same way as any proof, right? Check that each step is valid; in this case, that the symbol manipulation obeyed the rules.
What a mathematician[0] thing to say. This sounds like an isomorphism of "it's solvable in principle."
[0] Speaking as a scientist.
[0] Speaking as a scientist.
200 TB is not a lot, though, for a single pass validity check today. A core does roughly a billion operations per second and we have tools now for easy provisioning of computation power and distribution of work.
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.
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.
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.
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.
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...
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
Apologies for being nasty
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.
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.
Even for integral/rational solutions, the problem is still Turing complete since there may be no solution at all.
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
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.
I suspect the average mathematician won't consider that "elegant".
Well, the average mathematician can't define what they mean by "elegant" either.
Sure, but so what?
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.
>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.
Not really. All kinds of non-elegant, 80 and 200 page proofs (a proof doesn't have to be brute force to be inelegant) are regularly churned and appreciated every day.
Those are in fact the bread and butter of mathematics in practice, not the few and far between elegant proofs people read about.
Not really. All kinds of non-elegant, 80 and 200 page proofs (a proof doesn't have to be brute force to be inelegant) are regularly churned and appreciated every day.
Those are in fact the bread and butter of mathematics in practice, not the few and far between elegant proofs people read about.
This isn't really true. Many proofs often start as dozens or hundreds of pages long, yet the creator is credited with advancing mathematics. It isn't till later that someone else comes along and simplifies the proof.
But the thing which constructs the proof might be what we will consider to be an "elegant proof." It might be more unsatisfying not being able to understand exactly why something is true, but computers can greatly expand the reach of what we can know.
Haha this is the first thing I've heard about mathematics that reminds me of statements I've heard about chess. It's interesting to imagine a future in which useful math supporting useful tech is done by brutish AIs, while elegant math is the last refuge of humanity.
Can't these proofs be useful in the context of "given that X is true we can say that"? In that case it doesn't matter how X was proven, it just provides a tool for future mathematics.
Ultimately, in mathematics it is important to understand why something is true; simply knowing that someone (or something) "says so" is never good enough.
True, you don't understand why this is true. But you can understand that other things are true because this is true.
[deleted]
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?
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...
https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...
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.
[deleted]
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.
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.
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.
Sometimes I imagine that if we had much larger short term memories, an argument with only 633 cases would be obvious.
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
Yes, I think you are correct. I looked at it, and I looked into it, but only to grasp the general gist of it. The point was that essentially they reduced the infinite opportunities for tiling to a finite set of graphs whose composition covered the full spectrum of cases.
Everyone already strongly suspected that the FCT was true. Nobody was surprised by the result, it just took a computer to prove it.
You clearly are not a mathematician (nor am I). There's a huge, unimaginably broad chasm cognitive chasm between "suspected", "conjectured", and "proved".
There is, according to quite a few, also a huge etc. chasm between 'proved' and 'proved by a computer'. Especially if it's a proof through exhaustive enumeration.
I disagree wholeheartedly. Proof by enumeration of finite cases is the most iron clad and idiot proof form of proof one can possibly aspire to. Proof by enumeration is fine and dandy. Some might cast a pall of disreputability upon a proof by enumeration by computer, but really it is no different — the computer and its program are merely a formal system somewhat more complicated and thus harder to inspect than mathematicians are used to, but this does not pose any real conceptual disconnect.
I understand the difference between the concepts. Im just saying the FCT result was not a 'surprising one', which the poster I responded to was implying.
I hesitated before clicking on that link as for a second I thought it would start downloading that 200 TB proof.
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.
Did not see it, shouldn't you use an adblocker at work for obvious reasons?
sorry didn't see that. ad blind-ness.
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.
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.
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.
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.
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.
I don't want a math paper detailing 200TB of data. I want a paper telling me the generation of the digital input, the method that was used to actually prove it if it's novel. I want the authors to show how they verified the result and if it's important how they verified the automatic verification. The paper will end with "Oh and by the way, we used this conjecture because it was difficult, it's true. You can verify it yourself."
I want this all so I can do this myself, so I can prove a run-of-the-mill conjecture and not waste my time with it. I want this because proving is difficult and there is more to SAT than mathematical proofs, it is used in the industry. I want this because I trust a verified proof that the airplane won't crash more than a human proof.
The availability of computer proofs does not devalue the study of mathematics.
I want this all so I can do this myself, so I can prove a run-of-the-mill conjecture and not waste my time with it. I want this because proving is difficult and there is more to SAT than mathematical proofs, it is used in the industry. I want this because I trust a verified proof that the airplane won't crash more than a human proof.
The availability of computer proofs does not devalue the study of mathematics.
https://en.wikipedia.org/wiki/AdS/CFT_correspondence
In case anyone else had no idea what the parent was talking about.
In case anyone else had no idea what the parent was talking about.
I still have no idea :)
Wikipedia on Quantum Physics is usually pretty atrocious, and this page is no exception. It reads like... well, nerds showing off knowledge. (There's nothing wrong with that, but unless you're already pretty steeped in things quantum, the page is jargon without meaning)
A more readable summary: http://whystringtheory.com/toolbox/ads-cft/
Wikipedia on Quantum Physics is usually pretty atrocious, and this page is no exception. It reads like... well, nerds showing off knowledge. (There's nothing wrong with that, but unless you're already pretty steeped in things quantum, the page is jargon without meaning)
A more readable summary: http://whystringtheory.com/toolbox/ads-cft/
> Wikipedia on Quantum Physics is usually pretty atrocious, and this page is no exception. It reads like... well, nerds showing off knowledge.
Indeed. Wikipedia on math in general is useless unless you already understand it.
Indeed. Wikipedia on math in general is useless unless you already understand it.
aisofteng(1)
> 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.
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.
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.
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.
Lots of situations where the result obtained is only thing that matters to most users.
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.
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.
Not really
A proof that works is the most important part. After that you can make it nice
A proof that works is the most important part. After that you can make it nice
> you can make it nice
Not the 200 terabyte one, you can't.
Not the 200 terabyte one, you can't.
I have a couple of experiences of doing similar big projects where we counted the number of some objects (I haven't checked how big they are.. I have run SAT solvers for a couple of weeks, I didn't try to record some "proof size", I imagine it would be as big if not bigger than 200 terabytes).
Once I could tell a mathematician the count, in both cases someone they proved the result in an alternative way fairly soon afterwards :)
Once I could tell a mathematician the count, in both cases someone they proved the result in an alternative way fairly soon afterwards :)
Maybe we can use the brute force of a "math superoptimizer" to "compress" it to something far more reasonable. If we teach said opimizer what structures are well understood by humans we might actually understand at last parts.
I don't know why people keep thinking there's something special about the way we humans do calculations vs what could be achieved with a complex enough computer
Math is not about proofing something, or creating a as big as possible collection of lemmas. Math is about creating structures that can use as tools to solve problems. And problem solving is a task done by humans, so math is only useful if humans understand it and have a intuition.
These are not mere calculations. See, an understandable proof has more structure than plain first order logic alone. This allows such proofs to be extended and worked upon as well as real life implications to be discovered.
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.
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).
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).
Start now and make your altcoin, seriously :)
Err—presumably the proof that makes sense is a correct proof. How is that not a binary quality?
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.
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.
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".
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".
Well, that's a great explanation about why I didn't go into maths—I don't give a damn about how I arrived at knowledge so long as I can rely on it.
If and when most of the heavy lifting in the field of doing proofs will be done by computers, I suspect a new definition of proof will emerge not too far from what you're saying.
Rene Descartes or Isaac Newton would throw a fit if they could see this.
Rene Descartes or Isaac Newton would throw a fit if they could see this.
How do you know you can rely on it tho'? Blind faith?
I am stockpiling industrial amounts of popcorn for the (not too distant) future debates around the question: should we take into account the inherently limited capabilities of the human mind when defining the concept of "proof"?
To be sure, myself I am very much a classicist of the old school when it comes to such matters. But this is a brave new world we are slowly but surely moving into.
To be sure, myself I am very much a classicist of the old school when it comes to such matters. But this is a brave new world we are slowly but surely moving into.
That is correct as long as you don't hit the corner cases.
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.
Is that particularly valuable, though? It seems like a pretty anthropic point of view to value an algorithm as more elegant just because inferior hardware is able run it.
It's been a historically valuable heuristic -- algorithms/theories that provide cognitive scaffolding allow us not only to solve related problems but reason about the limits of applicability of that theory, successively guiding discovery of new theory. Obviously our cognitive envelope doesn't just include our own brains but the tools we use, including computational ones, so it's not as if pure proof/pure prediction don't also have value for guiding discovery, but it does require a lot of ingenuity to find ways to exploit them.
> 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?
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?
>> 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.
>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.
Isn't tossing a bunch of computational resources at a problem a new way of viewing it that makes it trivial?
But it gives no framework for approaching other problems under any kind of new unified theory.
Instead it gives a framework that will solve fairly arbitrary problems as you work on developing a unified theory. Techniques can be much more broadly useful than theories.
When I was working on my PhD, I probably saved days or weeks of effort by writing a program to brute force an approximate solution to an equation I couldn't work out. After seeing that the solution wasn't what I wanted, I was able to spend the time I would otherwise have spent on figuring out the equation on something more useful.
When I was working on my PhD, I probably saved days or weeks of effort by writing a program to brute force an approximate solution to an equation I couldn't work out. After seeing that the solution wasn't what I wanted, I was able to spend the time I would otherwise have spent on figuring out the equation on something more useful.
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.
That wouldn't be a proof though. The article is about exhausting the problem space rather than a probabilistic approach.
>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.
Not what I'm saying. I would suggest that absolute certainty is impossible wrt verifying conventionally proved theorems as well.
I think you moved the goal posts and are now talking about philosophy, not math. If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here?
> are now talking about philosophy, not math
Call it what you will.
> If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here?
One crucial difference is that our confidence level in a given proposition will be made explicit and will be quantified. I think you are misinterpreting what I'm saying as well-- the "experiments" I'm suggesting are not naive monte carlo simulations or tests of a nonexhaustive sample of special cases, but the generation of formal logical proofs (although not necessarily limited to that). The uncertainty would arise physically from the largeness of the computation, and once that barrier is crossed, it's conceivable that other (less rigorous) methods could be added to the battery of techniques as well (thereby increasing confidence). Also note that the size (amount of information) of the theorems and proofs would be large, and perhaps will surpass human comprehension, even after multiple stages of approximation and abstraction. The degree of confidence in such theorems would also be close to certainty as well. No human readable proofs would be harmed in the process, except for the false ones!
Call it what you will.
> If you are saying all math is probabilistic even with conventional theorems, how can you predict a future of probabilistic math if it's already here?
One crucial difference is that our confidence level in a given proposition will be made explicit and will be quantified. I think you are misinterpreting what I'm saying as well-- the "experiments" I'm suggesting are not naive monte carlo simulations or tests of a nonexhaustive sample of special cases, but the generation of formal logical proofs (although not necessarily limited to that). The uncertainty would arise physically from the largeness of the computation, and once that barrier is crossed, it's conceivable that other (less rigorous) methods could be added to the battery of techniques as well (thereby increasing confidence). Also note that the size (amount of information) of the theorems and proofs would be large, and perhaps will surpass human comprehension, even after multiple stages of approximation and abstraction. The degree of confidence in such theorems would also be close to certainty as well. No human readable proofs would be harmed in the process, except for the false ones!
I assume (perhaps incorrectly) that the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human, so I am further assuming that the potential for uncertainty you are positing comes from machine error (especially since you use the term "physical"). Are you aware of the rate of physical error in modern CPUs, memory, and storage technologies when they are arrayed in a redundant fashion? It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates. Furthermore, were this to be replicated by someone else on another set of machines, the likelihood of the same bit flip due to physical error is so unlikely as to be astronomical in its probability.
>the terrabytes of data generated by these computational proofs are created using an algorithm that has been proven correct by a human
Was thinking much bigger than that. Probably won't be feasible in the near future, and would of course be directed by very clever agents (mathematicians), themselves having excellent mathematical insight.
>It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates.
That's the idea. Replace "practically impossible to discover or know" with knowing to an astronomically high degree of certainty. Never suggested otherwise.
Was thinking much bigger than that. Probably won't be feasible in the near future, and would of course be directed by very clever agents (mathematicians), themselves having excellent mathematical insight.
>It is extremely low, and very unlikely even for a data set of this size, especially when compared to human error rates.
That's the idea. Replace "practically impossible to discover or know" with knowing to an astronomically high degree of certainty. Never suggested otherwise.
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.
In my experience, when a computer proof disagrees with a person proof, it's more likely the person was wrong, rather than the computer (along with the computer's programmer and hardware of course).
I don't think that's what he's saying though. He's talking about empiricism. But let's address your point. Couldn't a mind malfunction as well?
Sure it can. As an example, d'Alembert "proved" the Fundamental Theorem of Algebra but based his work on some assumptions that made the proof incorrect. So did Euler.
Correct proofs came much later thanks to Lagrange and (especially) Gauss.
Problem is: a smart guy can catch a malfunctioning in another smart guy's line of reason. Can they catch an error in 200TB of proof?
Problem is: a smart guy can catch a malfunctioning in another smart guy's line of reason. Can they catch an error in 200TB of proof?
> Can they catch an error in 200TB of proof?
Yes, you could either put an army of people on picking through the data, or write another software program that also picks through the data
In either case, we are talking about two different things. The initial discussion was about probabilistic theorems, which is the idea of throwing a bunch of tests at a problem and getting a sense of how likely it is that the theorem is correct vs going through the entire space of a problem through brute force.
Then somehow the discussion changed to whether people and computers can be trusted to not make mistakes when brute forcing the problem space, which is an entirely different subject from the topic of this post.
Yes, you could either put an army of people on picking through the data, or write another software program that also picks through the data
In either case, we are talking about two different things. The initial discussion was about probabilistic theorems, which is the idea of throwing a bunch of tests at a problem and getting a sense of how likely it is that the theorem is correct vs going through the entire space of a problem through brute force.
Then somehow the discussion changed to whether people and computers can be trusted to not make mistakes when brute forcing the problem space, which is an entirely different subject from the topic of this post.
The low probability of machine failure, combined with error correction means that by 4 layers of error correction, the chances of a failure (4 successive failures) are essentially nihil.
And furthermore, you could run it on different machines and have humans verify the results. In any case I'd trust the machines more than a human mind when it comes to consistency, and we already trust human minds with proofs.
I can't wait for the day when a proof is 'discovered' that no one can comprehend.
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.
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.
>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.
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.
Peter Norvig, 2011: On Chomsky and the Two Cultures of Statistical Learning
http://norvig.com/chomsky.html