I haven't watched the video, but I just have to get the word out
https://arxiv.org/pdf/2610.08144
From the abstract:
(...) we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean 'verifications'. These include OpenAI’s announced Navier-Stokes proof.