My solutions to the Reintroduction to proofs lean game. Most of the code uses term-mode proofs, except proofs for initial worlds (type_world, function_world and implication_world) which use simple tactics like assumption, apply.
This project uses Lean 4 and the Lake build system. Because it is built entirely from first principles, it features an incredibly lightweight workspace with zero external mathematical library dependencies (no Mathlib required!).
Ensure you have elan (the Lean version manager) installed on your system.
- Installation: Follow the official step-by-step setup guide at Lean deployment instructions for elan.
The exact compiler version will be automatically resolved using the repository's local lean-toolchain file the moment you run a build command.
To compile and type-check the entire repository across all proof worlds:
- Clear out any previous build caches:
lake clean
- Build and verify all the proofs
lake build