Let me get right to the point without any nonsense about aliens: Claude Code, the new AI coding agent from Anthropic, is pretty good at interactive theorem proving (ITP). I find this very surprising, and you probably should too. 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 I...