Monthly Archives: December 2015

The Lean Theorem Prover

Posted on 2 December 2015 by Floris van Doorn

Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code … Continue reading →

Posted in Code, Higher Inductive Types, Programming | 48 Comments