Sharing my thoughts, and code, as I develop a library of mathematics written in, and formally verified by, the Lean programming language and proof assistant. As well thinking about writing mathematics in type theory, I am also interested in writing about proof assistants and the underlying lambda calculi and type theory.
I am taking a lot of inspiration and code ideas directly from Mathlib and the Agda Standard Library. I make no claim of any novelty in this library, it is here purely for study and explanation. Helping myself, but maybe some readers too!
If you have found yourself here and want to comment on what I am doing, then please feel free to do so. Any criticism and clarifications are welcome.
Posts
subscribe via RSS