Terence Tao: Using modern tools to semi-automatically formalize a proof in Lean