This repository is currently a playground for the team at zkSecurity to explore and master Lean.
Its intended to become our monorepo for Lean utilities, libraries, etc.
Follow official instructions to install elan (the package manager) and Lean4.
Clone this repo, and test that everything works by building:
lake buildAfter that, we recommend open the repo in VSCode to get immediate inline feedback from the compiler while writing theorems.
Make sure to install the lean4 extension for VSCode!