21–30 of 61 posts
Jean-Yves Girard says that true theorems have corollaries. Computers can prove all sorts of propositions , but the gooey philosophical question is -- which propositions are Theorems in the grand civilizational project of mathematics?
Yes, the job of a mathematician is not to prove theorems. But rather to find the interesting or beautiful ones.
ctrl+F Gödel ctrl+w
Imagine, if you will, that you are addressing an audience that knows what Gödel's results are. In particular, assume that we know Gödel's proof that any formal system that's sufficiently complex to hold a model of arithmetic has statements that are true, but unprovable within the system.
Now, can you explain to us why this result makes it pointless to read the article?
If you prove something in Lean, can you automatically convert the proof into a Coq one (even if it looks like uglyfied/minified code)?
It feels like it should be possible to "merge" the proof repositories of these languages together into a common one.
Or to put another way, if you can prove in Coq that Lean is correct, then it should imply that Lean proofs are correct too.
I'm working on a forthcoming series of blog posts investigating FP concepts from scratch in Lean to see how it takes with the FP-curious.
The refreshing features Lean has to offer over other FP languages like Haskell is that
1. It's dependently typed which gives it a lot more flexibility to define objects that depend on types and types that depend on values, such as vectors that know their size.
2. Lean is interactive by default -- type inference is really fast, even for complex objects and functions.
From my perspective Lean is a great programming language that happens to have a theorem prover available. This, in itself, can be a great feature for code that needs to provide strong guarantees about its operational parameters.
The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (yes). Computer can also search for theorems and proofs to those plausible theorems. There are issues, of course. Both of these spaces are very, very large. It's not clear what makes for an "…
The fact that it is possible for a given proposition P to be neither provable nor disprovable has nothing to do constructive mathematics. This happens in classical mathematics as well – in any incomplete theory. All theories which serve as foundation of mathematics are incomplete (ref. Gödel).
It is just that a constructive mathematician can be at peace with this situation, since they does not believe P ∨ ¬P to be a tautology – while a classical mathematician will forever be tormented by the existence of theorems they cannot prove in their chosen formalism.
The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (yes). Computer can also search for theorems and proofs to those plausible theorems. There are issues, of course. Both of these spaces are very, very large. It's not clear what makes for an "…
> Unfortunately, most of these proving languages are constructive and thus it's possible for both of those to be unprovable. The fact that it is possible for a given proposition P to be neither provable nor disprovable has nothing to do constructive mathematics. This happens in classical mathematics as well – in any incomplete theory. All theories which serve as foundation of mathematics are incomplete (ref. Gödel).…
As a devotee to the law of excluded middle myself, I don't feel particularly tormented by this.
(I agree with your wider point that constructivism isn't the root cause of independent statements in mathematical foundation theories.)
There exists the software Coq which is a theorem prover. https://en.wikipedia.org/wiki/Coq
EDIT: Main difference between the two is that with a proof assistant, you write a proof and the assistant checks its correctness, while a prover provides you with a proof of a proposition's correctness (or of its lack thereof).
The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (yes). Computer can also search for theorems and proofs to those plausible theorems. There are issues, of course. Both of these spaces are very, very large. It's not clear what makes for an "…
Adding to black_knight's point, it's worth noting that even in complete theories this often isn't very heartening: interleaving searches for P and for (not P) will often take an enormous amount of time.
Even cleverer strategies can be hopeless. For example, the theory of real closed fields is complete (and hence by your interleaving argument, decidable), but appears to be EXPSPACE-complete (at least from a brief skim of the literature), hence known to be truly intractable. If standard complexity-theoretic conjectures hold up (e.g. P != NP, NP != coNP), then non-gargantuan proofs in proof systems for a wide variety of interesting problems will turn out to be both intractable to locate and incomplete.
None of this is to say that automated theorem proving can't or won't rise to the level of human mathematical activity (I think it will fwiw), but we need to be far cleverer about it.