5 ms·

> I still think we can have our cake and eat it too, but I'm not sure. I think if the purpose is merely to transmit proofs and axioms unambiguously, I think we

> I still think we can have our cake and eat it too, but I'm not sure. I think if the purpose is merely to transmit proofs and axioms unambiguously, I think we can have a language that performs just that and nothing else. I think stuff like this exists, but I don't know why it isn't the standard to publish with it. Math papers are written with high compression using standard tables of translations to reduce the processing load when trying to manipulate several things at once.

makmanalp 13y ago
But why present these in English, where you have to manually apply those tables of translations, knowing full well that humans are error prone? Why not use a computer readable and standardized language like coq / gallina (http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Coq), where you can verify the proof unquestionably and immediately AND you can use a compiler to translate the theorem into latex / english / whatever form you want immediately? If the "standard tables of translations" really exist and are really as standard as you claim, this method is clearly superior and that table can be utilized to translate to "mathematician lingo" if people still desire to stick to that.
- DerpDerpDerp 13y ago
  They're generally published in symbols, which largely have a direct translation in to more formal methods, with the English being included to comment on the motivations, things which might not be formalized in the theory, etc. The primary purpose of mathematics papers is for distributing information between mathematicians in a form which it's easy for them to integrate in to reasoning about new theorems. To reason about new theorems, you really want as many ideas/concepts to be able to be present in the mathematician's head free of context (ie, with the structure represented, but ignoring the traditional intuition about what it is or used for, which English naming can bias towards). Part of the problem of Coq is that you'd have to formalize a lot of the metatheory in to something computable, and we've been struggling to find a good approach to that since the 40s/50s. We have a lot of trouble with trying to formalize the axioms in a way that you can compute results from them. (Axiom of choice + axiom of excluded middle can cause problems in Coq, for instance.) A secondary concern is that the translations from full sequences of axiomatic steps to constructs which are higher level (ie, built on the idea that some axiomatic steps must exist in this instance, but we haven't found them explicitly) can be really complicated, as well as much bulkier. A math paper is usually no more than tens of pages, while a computer proof of a theorem can run in to the thousands.
  - makmanalp 13y ago
    Your reply is fascinating - the part about size difference and the difficulty in expressing certain things in theorem provers. About the size difference, I don't understand why it takes so much longer. What is so fundamentally different about Coq (or E or whatever) that it takes so much more space that just specifying it with mathematical notation? Is it because you have to start from scratch? Has no one created a "standard library of existing theorems / proofs" that one can depend on? Or is it because mathematical notation is just that much more expressive? So if verifying proofs is that difficult, what the heck are mathematicians doing when they read a paper? Not really actually verifying the proof? It's hard to believe that verification is one of those things that humans are just better at. (As opposed to, say, formulating new ideas, which is fundamentally difficult for computers) What is it that is so fundamentally difficult about verifying proofs formally, when a mathematician can just read a paper and call it done? If provable theorems are too hard, why don't we simply just start with a parseable mathematical notation standard? It's be pretty similar conceptually, but would be standardized. Surely that's not too difficult? That could still serve as the portion of the paper that is the "transmitting new findings formally" part, whereas the remaining part can be devoted to explanation.
    - DerpDerpDerp 13y ago
      You seem to imply that mathematical notation should be standardized, but are omitting that even languages explicitly meant for computation are not. Why do you think mathematics should be more standardized than programming? (Actually, I'd argue it's already more standardized than programming, and you're arguing for some kind of extreme position.) Sorry, forgot to reply to part I had meant to: > Is it because you have to start from scratch? Has no one created a "standard library of existing theorems / proofs" that one can depend on? It's because we have essentially picked the parts of mathematics we're going to force to be true about half way up the stack. If the axioms don't permit those theories, then we'll do away with the axioms and pick a different set. (And perhaps explore why they failed to, and what is required in axioms to enable those theorems.) As I mentioned before, mathematics already has a good way to relate high level theorems and such to these mid-level structures, and you see it employed all the time. The problem is that many of these structures aren't easy to compute with, so we're essentially having to work backwards to find a set of formalities that we can both do mechanistically and support the theorems/propositions we'd like to be true. Mathematicians generally don't evaluate the truth of a new paper relative to the axioms, but relative to the already established results in a field. So you question about why libraries don't exist is essentially "Why have mathematicians not replicated hundreds or thousands of years of effort in to a format that's hard for them to personally use, but is good for these tools we've developed in the past couple decades?" Well, people are working on it, but it's going to take some time. And the moment you pick a slightly different set of axioms, you need to rebuild large portions of the library you allude to, even if the results are still true. (Derivations in terms of base steps are considerably longer than most mathematics proofs would be, which often omit some "standard" kinds of details. For an idea of what this is like, read portions of Principia Mathematica by Russell and Whitehead.)

makmanalp 13y ago

But why present these in English, where you have to manually apply those tables of translations, knowing full well that humans are error prone? Why not use a computer readable and standardized language like coq / gallina (http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Coq), where you can verify the proof unquestionably and immediately AND you can use a compiler to translate the theorem into latex / english / whatever form you want immediately? If the "standard tables of translations" really exist and are really as standard as you claim, this method is clearly superior and that table can be utilized to translate to "mathematician lingo" if people still desire to stick to that.

DerpDerpDerp 13y ago
They're generally published in symbols, which largely have a direct translation in to more formal methods, with the English being included to comment on the motivations, things which might not be formalized in the theory, etc. The primary purpose of mathematics papers is for distributing information between mathematicians in a form which it's easy for them to integrate in to reasoning about new theorems. To reason about new theorems, you really want as many ideas/concepts to be able to be present in the mathematician's head free of context (ie, with the structure represented, but ignoring the traditional intuition about what it is or used for, which English naming can bias towards). Part of the problem of Coq is that you'd have to formalize a lot of the metatheory in to something computable, and we've been struggling to find a good approach to that since the 40s/50s. We have a lot of trouble with trying to formalize the axioms in a way that you can compute results from them. (Axiom of choice + axiom of excluded middle can cause problems in Coq, for instance.) A secondary concern is that the translations from full sequences of axiomatic steps to constructs which are higher level (ie, built on the idea that some axiomatic steps must exist in this instance, but we haven't found them explicitly) can be really complicated, as well as much bulkier. A math paper is usually no more than tens of pages, while a computer proof of a theorem can run in to the thousands.
- makmanalp 13y ago
  Your reply is fascinating - the part about size difference and the difficulty in expressing certain things in theorem provers. About the size difference, I don't understand why it takes so much longer. What is so fundamentally different about Coq (or E or whatever) that it takes so much more space that just specifying it with mathematical notation? Is it because you have to start from scratch? Has no one created a "standard library of existing theorems / proofs" that one can depend on? Or is it because mathematical notation is just that much more expressive? So if verifying proofs is that difficult, what the heck are mathematicians doing when they read a paper? Not really actually verifying the proof? It's hard to believe that verification is one of those things that humans are just better at. (As opposed to, say, formulating new ideas, which is fundamentally difficult for computers) What is it that is so fundamentally difficult about verifying proofs formally, when a mathematician can just read a paper and call it done? If provable theorems are too hard, why don't we simply just start with a parseable mathematical notation standard? It's be pretty similar conceptually, but would be standardized. Surely that's not too difficult? That could still serve as the portion of the paper that is the "transmitting new findings formally" part, whereas the remaining part can be devoted to explanation.
  - DerpDerpDerp 13y ago
    You seem to imply that mathematical notation should be standardized, but are omitting that even languages explicitly meant for computation are not. Why do you think mathematics should be more standardized than programming? (Actually, I'd argue it's already more standardized than programming, and you're arguing for some kind of extreme position.) Sorry, forgot to reply to part I had meant to: > Is it because you have to start from scratch? Has no one created a "standard library of existing theorems / proofs" that one can depend on? It's because we have essentially picked the parts of mathematics we're going to force to be true about half way up the stack. If the axioms don't permit those theories, then we'll do away with the axioms and pick a different set. (And perhaps explore why they failed to, and what is required in axioms to enable those theorems.) As I mentioned before, mathematics already has a good way to relate high level theorems and such to these mid-level structures, and you see it employed all the time. The problem is that many of these structures aren't easy to compute with, so we're essentially having to work backwards to find a set of formalities that we can both do mechanistically and support the theorems/propositions we'd like to be true. Mathematicians generally don't evaluate the truth of a new paper relative to the axioms, but relative to the already established results in a field. So you question about why libraries don't exist is essentially "Why have mathematicians not replicated hundreds or thousands of years of effort in to a format that's hard for them to personally use, but is good for these tools we've developed in the past couple decades?" Well, people are working on it, but it's going to take some time. And the moment you pick a slightly different set of axioms, you need to rebuild large portions of the library you allude to, even if the results are still true. (Derivations in terms of base steps are considerably longer than most mathematics proofs would be, which often omit some "standard" kinds of details. For an idea of what this is like, read portions of Principia Mathematica by Russell and Whitehead.)