Yeah, we really need LLMs to work swimmingly with Lean 4. It is currently hot garbage and it does not understand proof composition, exploring proof extensions, lemma search, etc. It does not explore an open-ended node to a mathematical knowledge graph by substituting various options.

I'd happily work with someone on a conversational theorem prover, if anyone's up for it.