The Coq Proof Assistant

Welcome ! | The Coq Proof Assistant

I've always been a bit warey of formal mathematical proof. Most of the people who I have met who make big claims for the power of mathematical proof always seem to have very dominant/dogmatic  personalities. While it may be a small statistical sample I do keep wondering if mathematical proof just appeals to people who's personality type is they can't believe they can ever be wrong. 

Still I like the notion of constructing 'truth' like lego bricks and like someone who goes to a modern art gallery but doesn't get the art but does appreciate the elegance which this work involve, I like the notion of proof.  My biggest doubt about the power of proof was that no one ever managed to make an automated proof system ( which if it wasn't partly based on 'I can't see my error so I must be right' theory of mathematical proofs). Or rather the automated proof systems so far have always failed to do anything but the most trivial work ( as far as I know).

So you can imagine how excited I am that someone has managed to generate a formal proof assistant. Obviously as someone who is big into human computer interaction I would be strongly in favour of a machine which will augment the process of thinking about mathmatics. The big problem apparently with this cog system is it needs a different type of proof to be based on types not sets. Still very exciting work.