I’m interested by this recent development where people are using LLMs with Lean to prove things that haven’t been formalized yet. This seems like a really good fit for LLMs. They’re good at translating approximate language to formal language, they’re good at information retrieval, and any failures are mitigated by Lean itself. I haven’t tried it, but I imagine failure modes might be proving useless lemmas along the way, taking a needlessly roundabout approach, or inadvertently proving something different than what you set out to do.