Coq and Lean are two of the most common proof assistants out there (but the question of course applies to other proof assistants too).
What are the main differences between Coq and Lean? Ideally it would be nice to know the differences for a mathematician not interested in foundations and for someone more involved in CS and type theory.
As to theoretical differences, the most thorough presentation I know of is found in section 2.8 of Mario Carneiro's master thesis, which I will try to summarize here:
fix and match constructs, where termination is ensured by additional typing rules, while Lean uses fundamental recursor functions that are inherently terminating.id @id typechecks. Coq has experimental support for it though.SProp of proof irrelevant propositions.
It it hard to write an answer here which is not just a technical list of differences in specification, but also avoids the flame war of "my theorem prover is better than yours". (I'd be happy to delete or change this answer if it comes across too flame-war-ish or incorrect.)
Lean is essentially classical, meaning it usually uses the law of excluded middle and the axiom of choice for proofs when it is convenient. This is mostly a social norm, in that this is the standard of the Lean community and main math library, mathlib. But it is also technical in a sense in that it is difficult to avoid classical reasoning with the common tactics (and basically impossible to do homotopy type theory even within term proofs). For many just interested in formalizing pure math (except of course, say, homotopy type theory or the internal logic of some topos) this is fine and maybe preferable. If you want more flexibility on axioms or want to be able to extract algorithms from your proofs it is a problem. (However, some projects in Coq also use classical reasoning, so it isn’t like it is forbidden. It just might mean that projects which use classical reasoning won't be used by other projects which are trying to stay constructive.)
There is also a difference in community goals. I can't speak to the goals of the Coq community, but it seems to me that the main goal of the Lean3 community is to add as much mathematics as they can to the mathlib library, the main mathematical library of Lean. There is a strong emphasis on unity and cohesion in this library. It is constantly refactored to make it work well together. This (according to Lean users) makes it possible to easily combine separate areas of mathematics like rings and topological spaces (to get topological rings), but it also means that any project which is not in mathlib or trying to stay up-to-date with mathlib will quickly bit-rot. (Even Lean3 itself---at least the community edition most commonly used---changes rapidly as well, sometimes in backward incompatible ways.)
We will see in Lean4 if the focus is the same or changes. Already, many are using Lean4 as a very capable programming language, so there may be more diversity of projects and less focus on cohesion, but nonetheless, I think the contributors of mathlib would like the Lean4 version to still be highly cohesive.
There is also a lot written on the internet about say Lean vs Coq. Of course note that since Lean and (to a lesser degree) Coq are constantly changing, some of that information may be out of date. (For example, there was a time when Lean 2 supported both classical and constructive logic, even homotopy type theory.)
