LeanEVM A toy implementation of the EVM in Lean4. Building In order to build the LeanEVM, you need to have the Lean4 toolchain installed (see here for instructions). % lake update % lake build This process can take a while to complete, as it compiles all of Mathlib.