We should write a compiler of Lean to the EVM. The best approach seems to be compiling it to Yul instead of the EVM directly. Yul is a first order language without function pointers and no jumps. To compile a higher-order program will then require us to write a function dispatcher. Thankfully, the paper on GRIN describes a way to make this efficient. The other things we have to consider is how objects (including closures) should be represented in memory so we can devise an allocator and a collector (which could be just refcounting)