Lean would be so well suited to LLMs. I hope we see a resurgence in interest in languages like that

Formal proofs have so much potential in this context