My personal anecdote is that I tried learning Lean 4 last year with a group of other smart and curious programmers, and after a couple of weeks of trying, we failed to make significant progress learning it and stopped. We had much better luck working with Coq instead.