Alpoge and Buckmaster publish finite-time blowup with smooth forcing for 3D Euler, Boussinesq and incompressible porous media

Sources: primary, assessment, repository, discussion
Summary: Tristan Buckmaster announced on his own account that he and Levent Alpoge proved finite-time blowup with a smooth forcing term for 3D incompressible Euler, the Boussinesq system, and incompressible porous media, which is not the unforced Navier-Stokes Millennium problem. The arguments are formalized in Lean, and the repository carries affinecore, boussinesq-blowup and euler-blowup directories. Terence Tao posted an assessment the same day naming the Cordoba and Martinez-Zoroa approach, confirming the Lean formalization, stating the arguments contain significant AI input that the authors spent recent weeks reworking into an acceptable form, and stating the authors released far earlier than planned because of external events.
Why it matters: The arguments are formalized in Lean and the code is public, so the AI contribution sits behind a proof checker rather than behind a claim, which is the standard the weaker AI-proof announcements of the past year did not meet.