Microsoft Research and CMU are developing a new theorem-prover, Lean. Here’s how they describe their goals:
The Lean Theorem Prover aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. The goal is to support both mathematical reasoning and reasoning about complex systems, and to verify claims in both domains.
It looks similar to Coq and Agda, but I’m not enough of an expert to provide a comparison.
What I find interesting is that in addition to a traditional, Emacs-based proof development environment, it also works in the browser. This should lower the barrier of entry for new users - I’ve seen a lot of complaints about how hard e.g. Coq is to set up (see my instructions if you’re using OS X).
I haven’t yet played around with it, but I hope to take a look at the tutorial soon.