I've often wondered how viable it is to use AI to fill out the ecosystem gaps in awesome but niche languages (still looking at you OCaml...).

I've not gone too deep down this train of thought because a standard library/ecosystem should be solid and I don't think LLMs are quite there... but if we can use LLMs+Lean maybe we can get the quality we need to bootstrap more of the Lean ecosystem?