Expositions / Supplementary material
Supplementary sources
Lean files accompanying selected notes, collected here alongside the full mathematical texts.
Each project download includes its Lean sources, pinned toolchain, dependency manifest, and project notes. The notes describe the formal statements and their relationship to the exposition.
Formalization scope and source notes
Build a project
With Lean’s elan toolchain manager installed, unpack a project and run the following from its directory. Its lean-toolchain file selects the required Lean version.
lake exe cache get
lake build