a) Thanks for putting this together!

b) Please don't hijack my scrolling.

c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.

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?