I've gone from zero knowledge of lean4 to the point where I'm doing most of my coding with it in ~6 months, and this was dramatically helped by how facile the AI assist is: it's remarkable how consistently fluent models are in lean4. I've found this to be true of the near frontier and smaller local models alike, LLMs just seem to get lean4.

I still have a ways to go before calling myself a lean4 expert, but I don't need assist to get useful programs anymore.

The ability to start with very little knowledge and still be able to trust parts you don't fully understand is a real unlock on learning progress: it's both practical and motivating to get useful programs you can rely on with incomplete knowledge, it sort of drags you in. You're bounded by the subset of the language that describes your axiom and proposition surface, not the subset that describes the intermediate steps. Over time as your ambition goes up, you need to understand more to do more things, but you can operate safely at level N+1 in a sense.

It's also just a delightful programming language irrespective of its theorem proving role, and it's remarkably fast. I've got it bolted to io_uring and in many cases it blows the ass off of C++ with libuv or Rust with Tokio. Now and again you'll see some huge tail at the p99.99 latency or something and you go make a number fixed width or something, but you have to tune C++ and Rust too.