Lecture: Blowup for the Euler Equations with Smooth Forcing – Tristan Buckmaster [video]

This is an excellent talk! Thanks for sharing!

Really interesting how they let agents write free-form text first(in what he describes as university exam level verbosity style), not Lean, and then at the end, when the agents claim to have found the proof, have other agents convert it to Lean and verify the proof there.

Recent recording from NYU Courant institute.