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.
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.