7 ms·
> Soon, they won’t consider a theorem proven until a computer has verified it. Is automated theorem proving really this close to being this powerful? So soon
by continuations 13y ago
> Soon, they won’t consider a theorem proven until a computer has verified it.
Is automated theorem proving really this close to being this powerful?
So soon we'd be able to feed the proof of Poincare Conjecture to a computer and it'd be able to verify the proof? I was under the impression we were nowhere close to being able to do that.
- pirriperdos 13y agoIt is not automated theorem proving, but computer verified proving
- ek 13y agoTechnically Coq is not a fully automated automated prover, but leaving that aside: We are definitely not even close. But getting mathematicians acquainted with HoTT is a good first step, I think. The book itself presents formulations of homotopy theory, set theory, category theory, and a constructive view of the real numbers, all within homotopy type theory, and on top of all this we could likely start building up a corpus of more results from topology, algebra, and analysis.
- byerley 13y agoI was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem
- joe_the_user 13y agoIt's easy for impressions of undecidability to get out of hand. But actually, verification is computable. Verification has to be computable for things like Godel's theorem to work. If you read your link carefully, you'll notice it's about provability via axioms, not verification. Peace
- jonahx 13y agojoe, what is the difference between verification and provability?
- tel 13y agoVerification is saying that a given proof does substantiate a theorem—it's easy as it's "just" a special kind of type-checking algorithm. Provability is saying that given some theorem it's possible to find a proof in a particular axiomatic system.
- lisper 13y agoIt's the difference between showing that a candidate proof is correct, and coming up with a correct proof in the first place. Once you have a proof, showing it is correct is (easily) computable. But coming up with a correct proof in the first place is not computable in general. (More generally, deciding whether a given proposition is true -- i.e. whether a proof exists or not -- is not computable. That is the "entsheidungsproblem".)
- jonahx 13y agothanks. after reading your explanation it's clear that the verification is verification of the proof, whereas i was interpreting it as verification of the statement to be proved, hence my confusion.
- joe_the_user 13y agoWow, Until I read your post, it never occurred to me you were confused by the ambiguous implications of "verification". You remind me how easy it is, once you get the jargon and the concepts, to not actually write out everything into a form someone from the outside can understand.
- jonahx 13y agoYeah, I personally file that under "Lessons You Never Learn Enough Times." Glad my slowness could be of service :) In retrospect, it seems like something I should have been able to deduce, since it's kind of the only thing makes sense.
- Chattered 13y agoIt's standard to use a verifier to check the correctness of a computer program, by encoding the program and then doing proofs about it. As per Goedel, a verifier can't check the correctness of its own program. So they'll always be incomplete there. Missing such a theorem isn't exactly a deal-breaker though.