Coq compcert Projects
The CompCert formally-verified C compilerProject mention: Proof Assistant Makes Jump to Big-League Math | Quanta Magazine | reddit.com/r/math | 2021-07-29
Again, the answer is "it depends"; there's even fragmentation between Lean3 and Lean4. Coq is very good at many things, such as verified compilers whilst Lean3 could never dream of such things. Lean4 is written in Lean4 so there's some hope for that. Meanwhile, a lot of maths has been written in both and they're both still actively used; I personally prefer Lean but that's personal preference. A "good" baseline to see mathematical progress in various proof assistants is Freek's 100 theorem list.