interview March 7, 2026 YouTube

Formalizing a proof in Lean using Claude Code

@TerenceTao27

Featuring

Terence Tao Professor of Mathematics, UCLA

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