Why Lean? I know Lean is interesting, but there's also Coq, Idris, Agda... And as others have pointed out, this would probably be a good use case for a lisp too.
Update: I just received my copy of the book, and at the bottom of page 4 the authors write:
“It would be an interesting endeavour to port the code from Haskell to a language with an even stronger type system, like Agda, Idris or Lean. The authors would welcome contributions in this direction.”
LEAN/Coq/Idris/Agda allow you to prove mathematical theories out of the box. Lisp not so much. Unless there is a Lisp library that gives you the power of Dependent Types and/or Refinement Types?