bluesky — HotBloodedHeroine — 8 Oct 2026
turns out openai might have vibed out a slop drive by millenium prize proof that makes basic mistakes like
#ai-assisted-mathematics #formal-verification #navier-stokes
turns out openai might have vibed out a slop drive by millenium prize proof that makes basic mistakes like
"We show that the formalised Lean proof does not correspond to the [written paper] proof of blow-up of solutions to the Navier-Stokes equations."
arxiv.org/abs/2610.08144