My first thought was why Lean vs Isabelle/HOL or Coq given all they have that can be leveraged? And selectively depending on how challenging or different you want your project.
As of right now, the project would probably be easier in Coq. But I'm confident that Lean 3 will eventually feature more powerful automation (and no Ltac). It is, after all, being developed by Leonardo de Moura, one of the creators of Z3.