Coq is an interactive theorem prover. I've been interested in it for a long time and I've written a few posts about it. I'm especially interested in Coq's usage in formalized mathematics. If you see interesting links about that, let me know!
- Finding that lemma: Coq search commands (2016-04-19)
- How to divide by zero? (2016-04-12)
- Elementary algebra in Coq: Trivial group (2016-03-01)
- Elementary algebra in Coq: Defining a group (2016-02-16)
- What's in a proof? (2016-02-09)
- Getting started with Coq (2016-02-02)
- Setting up Coq, Ssreflect and Proof General on OS X (2015-01-17)