Claude Can (Sometimes) Prove It

Let me get right to the point without any nonsense about aliens: Interactive theorem proving tools such as Lean are the most powerful and trustworthy kind of formal methods tool. They have been used to formally verify important things such as cryptographic libraries, compilers, and operating systems. Unfortunately, even experts find ITP proofs time-consuming and error-prone. That’s why it’s exciting—and very surprising!—to find that Claude Code is so good at ITP. Today, Claude Code can complete many complex proof steps independently, but it still needs a ‘project manager’ (me) to guide it through the whole formalization. But I think Claude Code points to a world where experts aren’t necessary, and theorem provers can be used by many more people. The rest of this post digs into what Claude Code can actually do. But if you’re interested in automated reasoning or formal verification, I recommend you stop reading, go sign up for Claude Code, Gemini CLI, Aider, Codex, or some other coding agent, and try it out on a problem you know well. It’ll cost about $20 / month for something useful, and maybe$100 / month for access to a state-of-the-art model. I reckon you’ll be able to get surprising successes (and interesting failures) with about two hours of work. (If you actually do this, email me and tell me how it went).