The Lean Theorem Prover

Something to do during your logical self-isolation: find out a little about The Lean Theorem Prover.

I confess I have previously never really “got” the supposed attractions of the likes of Coq. But I stumbled a week or two back over a piece by Thomas Hales on the pros and cons of using the much more recent Lean. There are a lot of cons, but still I was prompted to take a first quick look at the Lean documentation, and then stayed to read on quite far. As you might have predicted of something which Jeremy Avigad has a major hand in, this is really very well written. If you (like me) start with only a shaky grasp on why working in a version of dependent type theory might be a Good Thing, then this is interesting and genuinely illuminating –well worth looking at, even if you don’t find yourself playing with Lean itself for very long.

The post The Lean Theorem Prover appeared first on Logic Matters.