What's your favourite assisted theorem prover?

Question

Hi all,

I'm hoping to pick one of the many assisted theorem provers (rather than automatic ones) but there are rather a lot to choose from!

Does anyone have any you prefer and may I ask why?

Thanks!

Answer 1

Twelf, because it's based on LF, and I understand that well. Twelf can automatically make inferences based on structural induction, which can save a lot of work. The Twelf wiki is good.

Coq is probably the theorem prover that is most used for program verification these days, though, and is certainly the theorem prover most often discussed over at Lambda the Ultimate. Cf. a thread there: Course on Interactive Computer Theorem Proving Based on Coq, and take a look at the CoqArt book.

Which proof assistant is best for you depends pretty heavily on what you already know, and what you are trying to prove.