5 ms·

I like how the author mentions having an executable mathematical language might be helpful. Math is a non-standard non-machine-executable programming language w

I like how the author mentions having an executable mathematical language might be helpful. Math is a non-standard non-machine-executable programming language which means it's inherently buggy. On top of that, now I need to interpret the "code" while I'm learning and it can be pretty dense. Much like in programming, I'm sure expert mathematicians may not see why it's so painful, but wait until a more robust language/system is developed for the hobbyist. It will be extremely disruptive.

TelmoMenezes 13y ago
> Math is a non-standard non-machine-executable programming language which means it's inherently buggy. I don't understand what you mean by non-standard. I can't think of any language more standard than mathematics. Mathematical theorems are formally proven. That is a higher form of knowledge than empirical validation (running programs against tests). Another case of empirical validation is scientific experimentation. It validates theories by increasing our assessment of their plausibility, but never up to 100%. Mathematical proofs are the only completely objective form of knowledge. Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems.
- Dylan16807 13y ago
  >I don't understand what you mean by non-standard. Symbols in advanced math tend to be very poorly defined and contextual. Imagine programming if every function had a two-letter name and the list of which packages to import was left out half the time. This is covered in the article. Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form.
  - magicalist 13y ago
    > Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form. Just as important, though, is the number of proofs that anyone would want to read in that form. I can't think of anyone who has ever claimed that reading formally verified proofs aids understanding...
    - Dylan16807 13y ago
      Right, the current methods are probably awful for reading. It's a proof of concept more than anything, when it comes to using standard terminology.
- yummyfajitas 13y ago
  Mathematical theorems are formally proven. It's formal compared to colloquial english, but completely vague compared to computer programs. There are automatic theorem provers, but it isn't Godel's undecidability theorem that limits them. It's the difficulty of formally writing down our proofs in machine readable format that limits them for practical purposes.
  - karamazov 13y ago
    Mathematical proofs are completely precise, that is to say, not vague in the least. They are, however, in an extremely high-level language; it's left to the reader to expand the notation enough to convince themselves of the validity. (And, of course, there can be bugs - that is, mistakes - but there is no ambiguity.)
    - cwp 13y ago
      So the underlying ideas are precise, but they're expressed in imprecise language? That's true of all communication. When I ask my wife for "that thing by the door," I know exactly what I mean, but she has a to do a lot of work to decode it.
- dbaupp 13y ago
  > Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems Human mathematicians are equally limited by Gödel.
asolove 13y ago
What? Due to the Curry-Howard Correspondence, mathematical proofs are in fact very precisely executable: http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond... There may be lots of room to improve the "UI" of math [0] but I don't see how you could desire more power or verifiability than what modern mathematical proof systems offer. [0] http://worrydream.com/KillMath/ http://worrydream.com/KillMath/
- stygianguest 13y ago
  Only proofs in 'constructive' logic. There's a lot of proofs that aren't executable. Most importantly proofs by contradiction. See: http://en.wikipedia.org/wiki/Intuitionistic_logic http://en.wikipedia.org/wiki/Intuitionistic_logic In practical terms, however, this isn't a huge hurdle and comes with the nice advantage that you always have a program. BTW. I'm kinda sure you know this already, but I think it is important to mention. Thanks for the Haskell proof-book link. I'll check it out sometime.
  - magicalist 13y ago
    Hmm, I don't understand the problem. There is a philosophical question there, of course, but as long as you assume something like the law of excluded middle, you can easily set up a proof system allowing you to execute proofs by contradiction. This is a common strategy in Coq, for instance. Maybe I'm not understanding your point, though. I also don't think this chain of conversation is the sense that darkxanthos meant, either :)
    - thetwiceler 13y ago
      The idea is that the Curry-Howard isomorphism allows you to "play" with constructive mathematics easily. For example, consider the fact that the composition of two functions f and g is continuous if each function is continuous. Suppose f : X -> Y and g : Y -> Z. Then, in pseudo-Haskell syntax, we could say continuousf : Open set in Y -> Open set in X continuousg : Open set in Z -> Open set in Y continuousgf : Open set in Z -> Open set in X continuousgf = continuousf . continuousg The idea is that the fact that f is continuous means that we can produce open sets in X given open sets in Y. Now, consider the fundamental theorem of algebra over complex numbers. This says that any polynomial with complex coefficients with degree greater than 0 has at least one complex root. We'd like to have a function fta : Polynomial P of degree >0 over C -> (Point x in C, proof that P(x)=0) which would compute this root. But the thing is, the standard proof (e.g., by Louiville's Theorem) of the FTA is not constructive. The proof is by contradiction: Suppose there were no root. Then we violate some principle of complex analysis that we know is true (Louiville's Thm, or Maximum Modulus Principle, for example). Thus there must be a root. But this doesn't tell us at all how to compute the root! So instead we need a constructive proof of the FTA in order to produce a root. So, the idea is that you can't "play" with non-constructive mathematics in programming as you can with constructive mathematics. Our standard FTA proof would look like fta : Polynomial P of degree >0 over C -> Exists x. P(x)=0. But the type of the object that this function produces isn't very fun to play with. We have no idea what the root is!

TelmoMenezes 13y ago

> Math is a non-standard non-machine-executable programming language which means it's inherently buggy. I don't understand what you mean by non-standard. I can't think of any language more standard than mathematics. Mathematical theorems are formally proven. That is a higher form of knowledge than empirical validation (running programs against tests). Another case of empirical validation is scientific experimentation. It validates theories by increasing our assessment of their plausibility, but never up to 100%. Mathematical proofs are the only completely objective form of knowledge. Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems.

Dylan16807 13y ago
>I don't understand what you mean by non-standard. Symbols in advanced math tend to be very poorly defined and contextual. Imagine programming if every function had a two-letter name and the list of which packages to import was left out half the time. This is covered in the article. Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form.
- magicalist 13y ago
  > Proofs formatted for automatic solvers show that they can be standardized. Now think about the tiny percentage of proofs that are in this form. Just as important, though, is the number of proofs that anyone would want to read in that form. I can't think of anyone who has ever claimed that reading formally verified proofs aids understanding...
  - Dylan16807 13y ago
    Right, the current methods are probably awful for reading. It's a proof of concept more than anything, when it comes to using standard terminology.
yummyfajitas 13y ago
Mathematical theorems are formally proven. It's formal compared to colloquial english, but completely vague compared to computer programs. There are automatic theorem provers, but it isn't Godel's undecidability theorem that limits them. It's the difficulty of formally writing down our proofs in machine readable format that limits them for practical purposes.
- karamazov 13y ago
  Mathematical proofs are completely precise, that is to say, not vague in the least. They are, however, in an extremely high-level language; it's left to the reader to expand the notation enough to convince themselves of the validity. (And, of course, there can be bugs - that is, mistakes - but there is no ambiguity.)
  - cwp 13y ago
    So the underlying ideas are precise, but they're expressed in imprecise language? That's true of all communication. When I ask my wife for "that thing by the door," I know exactly what I mean, but she has a to do a lot of work to decode it.
dbaupp 13y ago
> Automatic theorem provers do exist and are employed by mathematicians, but they are inherently limited, as proven by Gödel's undecidability theorems Human mathematicians are equally limited by Gödel.

asolove 13y ago

What? Due to the Curry-Howard Correspondence, mathematical proofs are in fact very precisely executable: http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond... There may be lots of room to improve the "UI" of math [0] but I don't see how you could desire more power or verifiability than what modern mathematical proof systems offer. [0] http://worrydream.com/KillMath/ http://worrydream.com/KillMath/

stygianguest 13y ago
Only proofs in 'constructive' logic. There's a lot of proofs that aren't executable. Most importantly proofs by contradiction. See: http://en.wikipedia.org/wiki/Intuitionistic_logic http://en.wikipedia.org/wiki/Intuitionistic_logic In practical terms, however, this isn't a huge hurdle and comes with the nice advantage that you always have a program. BTW. I'm kinda sure you know this already, but I think it is important to mention. Thanks for the Haskell proof-book link. I'll check it out sometime.
- magicalist 13y ago
  Hmm, I don't understand the problem. There is a philosophical question there, of course, but as long as you assume something like the law of excluded middle, you can easily set up a proof system allowing you to execute proofs by contradiction. This is a common strategy in Coq, for instance. Maybe I'm not understanding your point, though. I also don't think this chain of conversation is the sense that darkxanthos meant, either :)
  - thetwiceler 13y ago
    The idea is that the Curry-Howard isomorphism allows you to "play" with constructive mathematics easily. For example, consider the fact that the composition of two functions f and g is continuous if each function is continuous. Suppose f : X -> Y and g : Y -> Z. Then, in pseudo-Haskell syntax, we could say continuousf : Open set in Y -> Open set in X continuousg : Open set in Z -> Open set in Y continuousgf : Open set in Z -> Open set in X continuousgf = continuousf . continuousg The idea is that the fact that f is continuous means that we can produce open sets in X given open sets in Y. Now, consider the fundamental theorem of algebra over complex numbers. This says that any polynomial with complex coefficients with degree greater than 0 has at least one complex root. We'd like to have a function fta : Polynomial P of degree >0 over C -> (Point x in C, proof that P(x)=0) which would compute this root. But the thing is, the standard proof (e.g., by Louiville's Theorem) of the FTA is not constructive. The proof is by contradiction: Suppose there were no root. Then we violate some principle of complex analysis that we know is true (Louiville's Thm, or Maximum Modulus Principle, for example). Thus there must be a root. But this doesn't tell us at all how to compute the root! So instead we need a constructive proof of the FTA in order to produce a root. So, the idea is that you can't "play" with non-constructive mathematics in programming as you can with constructive mathematics. Our standard FTA proof would look like fta : Polynomial P of degree >0 over C -> Exists x. P(x)=0. But the type of the object that this function produces isn't very fun to play with. We have no idea what the root is!