[dpah]

I've used Lean a fair bit (mostly contributing to mathlib), and have had a cursory glance at Coq. They are pretty similar, with really similar foundations. Both use variants of Calculus of Inductive Constructions for their foundation. Syntactically, Lean seems neater than Coq, and has more flexible pattern matching, and type inference.

It also has inbuilt support for quotient structures, which is a huge timesaver when dealing with Algebra. Might not be so important if you want to prove the correctness of programs. But I think the main advantage is that Lean is it's own meta-programming language, so you don't need to switch to Ltac/OCaml to write tactics.

The main advantage Coq has is it's code extraction feature. There was talk about implementing code extraction to C++ in Lean, but I don't think it has been done yet.

An oversimplified summary would be that Coq was designed with programmers in mind, while Lean was designed with mathematicians.

[xvilka]

It's notable, that Coq has more libraries and useful extensions. And they merged Ltac2 into the master, so tactics writing should be better soon.