Formalizing a proof in Lean using Claude Code

Tao demonstrates using Claude Code to formalize a mathematical proof in the Lean proof assistant