Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.