12 ms·

So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem wit

So, to me, proofs have two purposes. The first is to just say "This theorem is true". The second is to give some insight into the problem. I have no problem with such a proof satisfying purpose one; I may not be able to check it myself, but I can build a chain of trustworthiness all the way back to a program that I can check myself. In such a chain, the truth of the final result is not, to me, in dispute. Alas, such a proof throughly fails the second test. I can't see how to gain insight into the problem from such a proof, beyond just it validating previous thought chains of the form "If X were true, then I could deduce Y". It doesn't reveal more about the structure of the problem, or other results in the space. It's no doubt useful (and all credit to the authors), but in terms of generating new mathematics, I'm dubious. Perhaps people more versed in this specific sub-field can tell me if I'm wrong?

dragontamer 13y ago
It is a field of AI, not a field of Mathematics. Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician. At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct. http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...
- deleted 13y ago
  [deleted]
- ColinWright 13y ago
  I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations. In Haken and Appel's proof there was no automated reasoning. Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2. To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.
  - dragontamer 13y ago
    All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal. The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations. Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods. http://en.wikipedia.org/wiki/Automated_theorem_proving#Related_problems http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...
    - ColinWright 13y ago
      Knowing the FCT as well as I do, I have to say that I and many of my colleagues do not consider the H-A proof to be anything like automated reasoning. The work that Gowers and associates are now doing is very much so, but programming a computer to conduct a specific search, and for every item found compute whether it has a specific characteristic is really just like getting a machine to carry out a factoring algorithm. We run the risk of arguing past each other, and potentially being in "violent agreement," but consider this. If you take an 8x8 chessboard and remove any black square and any white square, the resulting mutilated chess-board is guaranteed to be exactly coverable by dominoes, each of which covers exactly two squares. We can program a computer to conduct an exhaustive search to show that this is true. Would you consider the program to be an automated reasoner? With what I know of this recent result, the work seems equivalent. It's a big problem fed to a SAT solver. Edit: See the last paragraph of section 1 in the paper: http://arxiv.org/pdf/1402.2184.pdf http://arxiv.org/pdf/1402.2184.pdf
      - dragontamer 13y ago
        Yes, although brute force would be "simple AI", but the basics of AI nonetheless. One of the many "classic" problems given to students of Artificial Intelligence is the 8-Queens problem: http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in_algorithm_design http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in... It is a short step to go from "8-Queens Algorithm Design" to "8-Queens Logic Programming", and from there automated reasoning. After all, Logic Programming is purely based on automated reasoning using Horn Clauses. It just so happens to be one of the most optimized forms of automated logic, fast enough to be a general programming language (Prolog is one of the easiest languages to solve the 8-Queens problem) Automated Reasoning covers new tricks, like tree pruning, different logic systems or methodologies (Tableau Logic)... but no matter how complicated it gets, it all comes back to the same methodology. Its simply a glorified search algorithm, defined over some space. (Prolog at its core is nothing more than a depth first search over the horn clauses specified by the programmer) For an example that clearly demonstrates the search, here's a Wikipedia link to Tableau type automated reasoning: http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Searching_for_a_closed_tableau http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Sea... And of course, the Automated Conference on the Tableaux Automated Reasoning methodology: http://en.wikipedia.org/wiki/International_Conference_on_Automated_Reasoning_with_Analytic_Tableaux_and_Related_Methods http://en.wikipedia.org/wiki/International_Conference_on_Aut... The "Art" of Automated Reasoning is not in the search methodology (which is almost always just depth-first search + heuristics), but in how to define those spaces. Horn Logic, Tableaux, First Order Logic / Resolution Rule, etc. etc. So whenever a new "search space" is defined to solve a practical problem, it is always of great interest to the Automated Reasoning community.
Someone 13y ago
I don't claim to be better versed in this field, but a way forward could be to do common subexpression elimination on this proof. Then, try and give names to those common subexpressions. Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.
- ColinWright 13y ago
  I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value. I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem. To me, what you say makes no sense at all. Perhaps this is what the field needs - people who know absolutely nothing making suggestions that are so far outside the box that those who have spent decades studying it would never consider them. On the other hand, maybe there's nothing in it. Have you thought it through more? Do you have more ideas? Do you have any actual concept of what "sub-expressions" might mean in this context? Having written compilers for food I feel that I have some knowledge of the concept, but in this case it seems not to mean anything.
  - peterderivaz 13y ago
    I wonder if you misunderstood his comment as a suggested method to solve the mathematical problem? The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.
    - ColinWright 13y ago
      The question then is whether there's any exploitable semantic structure in the certificate. I would guess not, but I don't have enough knowledge of the specifics of this problem and proof to be more certain. It just doesn't feel likely - any structure would emerge in the way the sub-sequences could be constructed, and lack of such structure is what makes this problem hard. Just a guess.
baddox 13y ago
In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?
- Pxtl 13y ago
  and now we're into questions about homoiconicity. I think I see why Lisp was so popular in AI research.
- ColinWright 13y ago
  Because the output of the program is effectively a long list of cases of things that have been considered[0], and why they do or don't "work" in some sense. The output is independent of the program and, in principle, can be checked. In some ways it's like printing the search tree of chess to show that white has a forced win. It doesn't matter if the program is "correct" - you can check the output separately. [0] EDIT: actually it's the certificate from a SAT solver
  - samatman 13y ago
    I believe "Someone" is wondering whether it's possible, and if so helpful, to work out the common factors in those search trees and give them names, much as a certain chess search tree could efficiently be called "Stonewall White" if it represented all boards reachable from that class of opening.
  - baddox 13y ago
    I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?
    - dllthomas 13y ago
      A CS prof I had held the position (in grading his tests - perhaps not generally) that "a proof is anything that convinces me you could write a proof". The program, along with an output saying "true", would seem to suffice under that metric.
ColinWright 13y ago
Absolutely - you seem to have nailed every point. The only thing you've missed is this - we now know that for C=2 the minimal length required to force a sub-sequence of discrepancy >=2 is 1161. The technique used gives a hint of how fast this dependency might grow, and that might give clues about techniques that probably won't work. It also seems clear that a similar brute-force check of C>=3 won't be possible. Knowing these things gives clues as to how we might now proceed.
brador 13y ago
Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?
- Houshalter 13y ago
  Presumably nothing. Unless you know how to program strong AI, and even then it probably wouldn't find anything interesting. There is no definition of what "interesting" is. It could discover tons of truths like "555 + 724 = 1279" but none of those would be particularly interesting to humans.
- arbitrage 13y ago
  Perhaps an infinite number. However, like a tree falling in the woods ... if humans (or some other intelligence) can't understand it, has anything actually been discovered? Or is it more like a computer algorithmically solving a jigsaw puzzle?
  - wlievens 13y ago
    What what? And, what the hell is an infinite number?
- baddox 13y ago
  That would prove to be insurmountably difficult: http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...
- zeidrich 13y ago
  It would "discover" every curiosity that we have yet to find, but it would be useless. Consider the universe. It is essentially a giant mechanical construct which works within the confines of every mathematical, physical, and even metaphysical truth. Imagine that you don't exist. Then what can you learn from the universe? The universe itself might "discover" everything. But that is meaningless to you. Now assume you do exist in the universe. What truths does the universe teach you? Only the ones that you witness and understand. If I come up with an incredible proof and write it down on paper and put it in my shirt pocket. Then I don't tell anyone until I die, and I'm cremated in the same shirt with the same proof, and my ashes are scattered across the ocean, what have I discovered? I only discovered something that was already true, I didn't bring the truth into existence, and while I didn't do anything with it nor share it with anyone it doesn't mean that it became any less true. But then what was the purpose? The purpose of a proof is to take a truth and to distill it into an idea that can be shared. A truth on its own is meaningless. If I say a^2+b^2=c^2, a lot of context is required, what do a, b, c mean? What sort of geometry does this work in? Why is this the case? Is it ever not the case? When every question is answered, and you are certain of that, then you have a proof. Just knowing that a^2+b^2=c^2 is meaningless. Even if I could prove that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse, that's still not completely meaningful, because it's not true in elliptic or hyperbolic geometries. But the abstract idea, that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse is Euclidean space is meaningful, because it leads to questions like "What would that mean about space if the sum of the squares of the lengths of sides of a right angle triangle were greater or smaller than the square of the hypotenuse?" and you start to consider alternative geometries. If a computer were to definitively prove that a^2+b^2=c^2 what does that mean if you can not really understand the implications of the proof. Yes it's true, but what does it mean? And why?
jkarni 13y ago
But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost say) how much more likely you are to prove something else (or how much easier it would be) -- without computer assistance. But the twist is that with computer-aided proofs, being well-versed in the ways of using computers to help prove things may begin to count as having insight; and Coq (or whatever) programs may come to be studied so that one may gain insight, just as human proofs are studied today.
deleted 13y ago
[deleted]
judk 13y ago
The case analysis demonstrates that the overall nontrivial strategy is correct. The insight is in the strategy.
lovemath 13y ago
A good mathematical proof is like a poem, not a telephone directory.

dragontamer 13y ago

It is a field of AI, not a field of Mathematics. Automated Theorem Proving is a very old field, one of the earliest fields of Artificial Intelligence. The first proof of this nature was the Four Color Theorem, proven by an automated reasoner as opposed to a mathematician. At which point, the insight into the matter is understanding the AI algorithm and how the AI searches for a solution. And finally... how we can be sure that the AI itself is provably correct. http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_com...

deleted 13y ago
[deleted]
ColinWright 13y ago
I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations. In Haken and Appel's proof there was no automated reasoning. Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2. To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.
- dragontamer 13y ago
  All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal. The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations. Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods. http://en.wikipedia.org/wiki/Automated_theorem_proving#Related_problems http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...
  - ColinWright 13y ago
    Knowing the FCT as well as I do, I have to say that I and many of my colleagues do not consider the H-A proof to be anything like automated reasoning. The work that Gowers and associates are now doing is very much so, but programming a computer to conduct a specific search, and for every item found compute whether it has a specific characteristic is really just like getting a machine to carry out a factoring algorithm. We run the risk of arguing past each other, and potentially being in "violent agreement," but consider this. If you take an 8x8 chessboard and remove any black square and any white square, the resulting mutilated chess-board is guaranteed to be exactly coverable by dominoes, each of which covers exactly two squares. We can program a computer to conduct an exhaustive search to show that this is true. Would you consider the program to be an automated reasoner? With what I know of this recent result, the work seems equivalent. It's a big problem fed to a SAT solver. Edit: See the last paragraph of section 1 in the paper: http://arxiv.org/pdf/1402.2184.pdf http://arxiv.org/pdf/1402.2184.pdf
    - dragontamer 13y ago
      Yes, although brute force would be "simple AI", but the basics of AI nonetheless. One of the many "classic" problems given to students of Artificial Intelligence is the 8-Queens problem: http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in_algorithm_design http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in... It is a short step to go from "8-Queens Algorithm Design" to "8-Queens Logic Programming", and from there automated reasoning. After all, Logic Programming is purely based on automated reasoning using Horn Clauses. It just so happens to be one of the most optimized forms of automated logic, fast enough to be a general programming language (Prolog is one of the easiest languages to solve the 8-Queens problem) Automated Reasoning covers new tricks, like tree pruning, different logic systems or methodologies (Tableau Logic)... but no matter how complicated it gets, it all comes back to the same methodology. Its simply a glorified search algorithm, defined over some space. (Prolog at its core is nothing more than a depth first search over the horn clauses specified by the programmer) For an example that clearly demonstrates the search, here's a Wikipedia link to Tableau type automated reasoning: http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Searching_for_a_closed_tableau http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Sea... And of course, the Automated Conference on the Tableaux Automated Reasoning methodology: http://en.wikipedia.org/wiki/International_Conference_on_Automated_Reasoning_with_Analytic_Tableaux_and_Related_Methods http://en.wikipedia.org/wiki/International_Conference_on_Aut... The "Art" of Automated Reasoning is not in the search methodology (which is almost always just depth-first search + heuristics), but in how to define those spaces. Horn Logic, Tableaux, First Order Logic / Resolution Rule, etc. etc. So whenever a new "search space" is defined to solve a practical problem, it is always of great interest to the Automated Reasoning community.

Someone 13y ago

I don't claim to be better versed in this field, but a way forward could be to do common subexpression elimination on this proof. Then, try and give names to those common subexpressions. Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.

ColinWright 13y ago
I've re-drafted this several times and it always seems to come out snarky. Please believe me that it's not intended as such - my field is mathematics, not English. So please accept this at face value. I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem. To me, what you say makes no sense at all. Perhaps this is what the field needs - people who know absolutely nothing making suggestions that are so far outside the box that those who have spent decades studying it would never consider them. On the other hand, maybe there's nothing in it. Have you thought it through more? Do you have more ideas? Do you have any actual concept of what "sub-expressions" might mean in this context? Having written compilers for food I feel that I have some knowledge of the concept, but in this case it seems not to mean anything.
- peterderivaz 13y ago
  I wonder if you misunderstood his comment as a suggested method to solve the mathematical problem? The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.
  - ColinWright 13y ago
    The question then is whether there's any exploitable semantic structure in the certificate. I would guess not, but I don't have enough knowledge of the specifics of this problem and proof to be more certain. It just doesn't feel likely - any structure would emerge in the way the sub-sequences could be constructed, and lack of such structure is what makes this problem hard. Just a guess.

baddox 13y ago

In this case, I don't see why the proof is considered to be the output of the program, but rather the entire program itself. If you can verify the soundness of the software and hardware involved (I certainly can't, but I presume the verification has been done), why should a human need to actually read the output?

Pxtl 13y ago
and now we're into questions about homoiconicity. I think I see why Lisp was so popular in AI research.
ColinWright 13y ago
Because the output of the program is effectively a long list of cases of things that have been considered[0], and why they do or don't "work" in some sense. The output is independent of the program and, in principle, can be checked. In some ways it's like printing the search tree of chess to show that white has a forced win. It doesn't matter if the program is "correct" - you can check the output separately. [0] EDIT: actually it's the certificate from a SAT solver
- samatman 13y ago
  I believe "Someone" is wondering whether it's possible, and if so helpful, to work out the common factors in those search trees and give them names, much as a certain chess search tree could efficiently be called "Stonewall White" if it represented all boards reachable from that class of opening.
- baddox 13y ago
  I get that, but all these articles are worried about the fact that no human could possibly read and verify the output of the program. So why even bother? Why not just verify the software and hardware that generates the output?
  - dllthomas 13y ago
    A CS prof I had held the position (in grading his tests - perhaps not generally) that "a proof is anything that convinces me you could write a proof". The program, along with an output saying "true", would seem to suffice under that metric.

ColinWright 13y ago

Absolutely - you seem to have nailed every point. The only thing you've missed is this - we now know that for C=2 the minimal length required to force a sub-sequence of discrepancy >=2 is 1161. The technique used gives a hint of how fast this dependency might grow, and that might give clues about techniques that probably won't work. It also seems clear that a similar brute-force check of C>=3 won't be possible. Knowing these things gives clues as to how we might now proceed.

brador 13y ago

Imagine if we could program a computer with all known mathematical truths. What curiosities would it discover that we have yet to find?

Houshalter 13y ago
Presumably nothing. Unless you know how to program strong AI, and even then it probably wouldn't find anything interesting. There is no definition of what "interesting" is. It could discover tons of truths like "555 + 724 = 1279" but none of those would be particularly interesting to humans.
arbitrage 13y ago
Perhaps an infinite number. However, like a tree falling in the woods ... if humans (or some other intelligence) can't understand it, has anything actually been discovered? Or is it more like a computer algorithmically solving a jigsaw puzzle?
- wlievens 13y ago
  What what? And, what the hell is an infinite number?
baddox 13y ago
That would prove to be insurmountably difficult: http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...
zeidrich 13y ago
It would "discover" every curiosity that we have yet to find, but it would be useless. Consider the universe. It is essentially a giant mechanical construct which works within the confines of every mathematical, physical, and even metaphysical truth. Imagine that you don't exist. Then what can you learn from the universe? The universe itself might "discover" everything. But that is meaningless to you. Now assume you do exist in the universe. What truths does the universe teach you? Only the ones that you witness and understand. If I come up with an incredible proof and write it down on paper and put it in my shirt pocket. Then I don't tell anyone until I die, and I'm cremated in the same shirt with the same proof, and my ashes are scattered across the ocean, what have I discovered? I only discovered something that was already true, I didn't bring the truth into existence, and while I didn't do anything with it nor share it with anyone it doesn't mean that it became any less true. But then what was the purpose? The purpose of a proof is to take a truth and to distill it into an idea that can be shared. A truth on its own is meaningless. If I say a^2+b^2=c^2, a lot of context is required, what do a, b, c mean? What sort of geometry does this work in? Why is this the case? Is it ever not the case? When every question is answered, and you are certain of that, then you have a proof. Just knowing that a^2+b^2=c^2 is meaningless. Even if I could prove that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse, that's still not completely meaningful, because it's not true in elliptic or hyperbolic geometries. But the abstract idea, that the sum of the squares of two sides of a right angle triangle is equal to the square of the hypotenuse is Euclidean space is meaningful, because it leads to questions like "What would that mean about space if the sum of the squares of the lengths of sides of a right angle triangle were greater or smaller than the square of the hypotenuse?" and you start to consider alternative geometries. If a computer were to definitively prove that a^2+b^2=c^2 what does that mean if you can not really understand the implications of the proof. Yes it's true, but what does it mean? And why?

jkarni 13y ago

But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost say) how much more likely you are to prove something else (or how much easier it would be) -- without computer assistance. But the twist is that with computer-aided proofs, being well-versed in the ways of using computers to help prove things may begin to count as having insight; and Coq (or whatever) programs may come to be studied so that one may gain insight, just as human proofs are studied today.

deleted 13y ago

[deleted]

judk 13y ago

The case analysis demonstrates that the overall nontrivial strategy is correct. The insight is in the strategy.

lovemath 13y ago

A good mathematical proof is like a poem, not a telephone directory.