Hacker News Reader

Comment by continuations | Hacker News Reader

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

View on HN

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

I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem

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

joe, what is the difference between verification and provability?

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

It'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".)

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

Wow,

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.

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

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

It is not automated theorem proving, but computer verified proving

Reply on news.ycombinator.com