Quanta: the Navier-Stokes proof was formally verified in Lean, and Fefferman names the real "heroes" as Córdoba and Martínez-Zoroa
Quanta Magazine·high signal
Quanta reports the singularity proof for 3D Navier-Stokes was machine-checked in Lean, adding 17 hours of formalization on top of the 88 hours of proof search. Princeton's Charles Fefferman credits Diego Córdoba and Luis Martínez-Zoroa as "the heroes of the story" for the analytical techniques the result rests on, and Córdoba notes that a decade ago "nobody believed there was a singularity for Navier-Stokes." Buckmaster himself concedes some of the AI output was "AI slop."