This Companion aims to formalise most of the definitions, theorems, and exercises in the second edition of Lawvere and Schanuel's Conceptual Mathematics using Lean 4 and mathlib.
The Companion has been written in Verso and is hosted at https://davidkinkead.github.io/conceptual_mathematics
Files containing just the unannotated Lean code for each Article and Session have been automatically generated by Verso and reside in the folder _out/cm/cm-code/ConceptualMathematics
A version of these unannotated files without solutions to the exercises (i.e., with the body of most definitions and examples in the exercises replaced by sorry) can be found in the folder ConceptualMathematics/Sorried
This Companion is the result of a project I undertook to learn both Lean and some elementary category theory at the same time (and ultimately a decent amount about Verso too). It remains a work in progress1. It will contain plenty of opportunities for improvement and more than a few errors! I welcome any comments, suggestions, corrections, or contributions. Please feel free to open an issue or a pull request.
Footnotes
-
At the present time, it is mostly complete through Session 29, so currently covers around three quarters of the book. ↩