My aim with this blog is to document the development of a small library of mathematics formalised in Lean. Explaining the mathematics and coding choices along the way. Most of the code I write is inspired by browsing both Mathlib and the Agda Standard Library. As this library is for my personal learning about proof assistants, the other two libraries will always be far more substantial. If you’re interested in writing proofs of even slightly sophisticated mathematics, then it is best to build on those libraries linked above. However, if you’re interested in learning about the process of formalisaing mathematics, then I hope to have something of worth for you here, in due course.

As well as blogging about mathematics in Lean, I also write about the mathematics underlying type theory based proof assistants. I will write on lambda calculus, type theory, and aspects of functional programming related to the development of such libraries.

Initial entries will be about developing the number systems that mathematicians are interested in, as well as the choices and code written to formalise them. In particular, the natural numbers, integers, rational numbers, and the real numbers.