Monthly Archives: December 2015

The Lean Theorem Prover

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 | 47 Comments