This is a repository for our explorations in theorem verification and homotopy type theory.
Mostly, it consists of Scott Morrison and Stephen Morgan tinkering with Lean, trying to understand just how hard it is to write real mathematics!
You may find useful the Getting started guide.
Everything is available under the Apache 2.0 license, as detailed in LICENSE.