But I think Claude Code points to a world where experts aren’t necessary, and theorem provers can be used by many more people. Claude Can Write LeanI used Claude Code to work on a Lean formalization of an old paper, Deny-Guarantee Reasoning (Dodds, Feng, Parkinson, Vafeiadis - 2009). I acted as a ‘project manager,’ directing Claude Code to work through the research plan step by step. Of course, the experiment I’ve described above isn’t Claude Code autonomously formalizing my old paper from end to end. Even more surprising, this capability doesn’t come from some fancy solver or novel algorithm; Claude Code wasn’t designed for theorem proving at all!