lean4 Playground Toying around with Microsoft Lean. Thematically related to my Coq Playground. To build the project, execute lake build Then run .lake/build/bin/lean-playground