Formalizing a proof in Lean using Claude and o4 - Terence Tao [video]