5 ms·

> Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. The short answer is that mathematics

> Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. The short answer is that mathematics is not actually a very good application for computation. It's a rather poor application for computation. Herein lies the rub and the reason why it can't be done as easily as you'd suppose. Computationally-oriented questions and theorems are a subset of all available mathematics research in the same way that computer science is only a subset of all available applied mathematics. Stated another way, imagine the massive difference of effort involved between developing an application that works and formally proving that your application works for all possible inputs. It's extremely difficult to take the set of all possible test cases and reduce them to a set of equivalence classes which can be individually proved. This is the difference between constructive and non-constructive proofs. Most mathematics is not actually constructive, which intrinsically presents a difficulty for computational theorem proving. Furthermore a lot of mathematics (particularly in the various flavors of analysis) is continuous in nature, which is inherently difficult for a computer to correctly model. For example, computers don't actually deal with real numbers, the floating points are just a good enough practical approximation of them. If you look at the noteworthy cases where computer-assisted theorem proving has done very well, they generally fall into one of two categories: 1. Cases where the program mechanizes a well-established theorem with a vast amount of scaffolding theory already existing around it. In this way it's relatively easier to automatically prove much of undergraduate mathematics, the bulk of which has been reduced to very succinct proofs over the past few centuries (undergraduate mathematics doesn't really make it past the late 19th century in terms of novelty). 2. Cases where a vast problem can be provably reduced to a large but finite number of special cases, each of which can then be individually proven. The four color theorem is an example of this variant of automated theorem. To give you an idea of how monumental the gap between research mathematics theorems and computation is: in order to make as much progress as we have, we've had to develop an entirely new theory of foundational mathematics (type theory). This allows us to bridge the gap between theorems and automated proofs in a way that set theory doesn't really allow. But that's a huge undertaking and a very quickly growing field of math. When it comes down to it, mathematicians do not tend to do research in, nor does their intuition naturally map to, a computationally rigid language. Essentially no current mathematician was taught or trained to do their research in a computational manner unless that was explicitly their field of research. Furthermore, while mathematical terminology looks formal to an outsider, there is a significant amount of symbolic overloading and notational interpretation in modern math. That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on."

thrmsforbfast 8y ago
> That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on." THIS is the real reason more mathematics isn't computer-checked. You massively buried the lede. > Most mathematics is not actually constructive, which intrinsically presents a difficulty for computational theorem proving How so? There are plenty of theorem provers for classical logics. > Furthermore a lot of mathematics (particularly in the various flavors of analysis) is continuous in nature, which is inherently difficult for a computer to correctly model. You can do continuous mathematics in a theorem prover. E.g. much of the classical theory of ODEs has been formalized in various theorem provers. Proofs about infinite structures are still a finite sequence of axiom applications. Furthermore, outside of theorem proving, numerical analysis and simulation of ODEs/PDEs is probably THE killer example of computers revolutionizing a field of mathematics... > For example, computers don't actually deal with real numbers, the floating points are just a good enough practical approximation of them. When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true. Integers aren't decidable: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Reals are deciable: https://en.wikipedia.org/wiki/Real_closed_field#Model_theory:_decidability_and_quantifier_elimination https://en.wikipedia.org/wiki/Real_closed_field#Model_theory... > To give you an idea of how monumental the gap between research mathematics theorems and computation is: in order to make as much progress as we have, we've had to develop an entirely new theory of foundational mathematics (type theory). Again, there's nothing stopping us from doing classical mathematics in a theorem prover.
- throwawaymath 8y ago
  > When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true...Integers aren't decidable...Reals are decidable I'm not talking about decidability. I'm talking about computability. Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed. But that has no bearing on the fitness of real numbers for computation. Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.

thrmsforbfast 8y ago

> That doesn't mean most proofs are wrong, but it does mean that most mathematicians are informal; to the extent they write down proofs of their theorems, they've only ever needed to do so enough to get other mathematicians to say, "Yes, I see what you mean, this does logically follow from what we already both agree on." THIS is the real reason more mathematics isn't computer-checked. You massively buried the lede. > Most mathematics is not actually constructive, which intrinsically presents a difficulty for computational theorem proving How so? There are plenty of theorem provers for classical logics. > Furthermore a lot of mathematics (particularly in the various flavors of analysis) is continuous in nature, which is inherently difficult for a computer to correctly model. You can do continuous mathematics in a theorem prover. E.g. much of the classical theory of ODEs has been formalized in various theorem provers. Proofs about infinite structures are still a finite sequence of axiom applications. Furthermore, outside of theorem proving, numerical analysis and simulation of ODEs/PDEs is probably THE killer example of computers revolutionizing a field of mathematics... > For example, computers don't actually deal with real numbers, the floating points are just a good enough practical approximation of them. When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true. Integers aren't decidable: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... Reals are deciable: https://en.wikipedia.org/wiki/Real_closed_field#Model_theory:_decidability_and_quantifier_elimination https://en.wikipedia.org/wiki/Real_closed_field#Model_theory... > To give you an idea of how monumental the gap between research mathematics theorems and computation is: in order to make as much progress as we have, we've had to develop an entirely new theory of foundational mathematics (type theory). Again, there's nothing stopping us from doing classical mathematics in a theorem prover.

throwawaymath 8y ago
> When you drill down into the model theory, you come to the amazing surprise that exactly the opposite is true...Integers aren't decidable...Reals are decidable I'm not talking about decidability. I'm talking about computability. Real closed fields are decidable, in that a Turing machine can determine in a finite number of steps whether or not a field of real numbers is algebraically closed. But that has no bearing on the fitness of real numbers for computation. Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated.