A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. Not to be used for requesting assistance on finding proofs.

learn more… | top users | synonyms

42
votes
9answers
4k views

How do they verify a verifier of formalized proofs?

In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. This is quite an ...
20
votes
4answers
3k views

Why is it so difficult to write complete (computer verifiable) proofs?

For example I have read that is agony to give a complete proof of the Jordan curve theorem. Since all statements are meant to be justified by the postulates, where does the difficulty lie?