4 ms·

> 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

> 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.

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.