Why3 ‘extends’ OCaml with similar features as well

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.

I'm trying to learn Lean and like it, but it's terribly lacking documentation.

The lacking good docs was what stymied my group too.