5 ms·

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

> 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
  > I'm not talking about decidability. If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures! Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions. > 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 No. Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals. If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand. If I want to prove something arbitrary about real closed fields, I can press a button and go for a run. Computers are much better at proving things about real closed fields than they are at proving things about integers! > I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated. One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms. This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)
  - deleted 8y ago
    [deleted]

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
> I'm not talking about decidability. If you are talking about theorem proving then you are most definitely talking about decidability! And especially if you are talking about wide-spread use of theorem proving (or lack thereof), then you are definitely talking about decision procedures! Decidable theories are easier to build formal proofs for than undecidable theories because the former requires only pressing a button and grabbing a coffee/lunch, while the latter requires hard work manually encoding bespoke deductions. > 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 No. Real closed fields are decidable, in that an implementable algorithm can in finite time and without a single iota of effort on the part of the user prove any arbitrary theorem stated in first-order logic over the reals. If you want to prove some arbitrary thing about Peano integer arithmetic, odds are fairly good that you're going to have to carefully program out the proof by hand. If I want to prove something arbitrary about real closed fields, I can press a button and go for a run. Computers are much better at proving things about real closed fields than they are at proving things about integers! > I'm talking about computability... Most real numbers are not computable, which is why floating point numbers are only a good enough approximation as I stated. One does not need to use a single float point in order to axiomatize the real numbers and prove things using that set of axioms. This has been done so many times that there are even survey papers about all the various approaches: https://hal.inria.fr/hal-00806920v1/document https://hal.inria.fr/hal-00806920v1/document (Floating points are a nice optimization and therefore many people care about them in practice so that they can take fewer coffee breaks during their theorem proving sessions, but again, they are not necessary.)
- deleted 8y ago
  [deleted]