Post

@arthur.clune.org

I predict there will be all sorts of issues buried in these proofs, but they will not change the long term course. Like counting letters in strawberry or basic errors in code

Gilles Louppe@glouppe.bsky.social

uh oh "We show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."

8/10/26, 11:32 am0 reposts1 like

Richard G Clegg

@richardclegg.bsky.social

Didn't this turn out to be something very minor like the text implied three parameters when there were four in the lean model.

Arthur Clune

@arthur.clune.org

Yeah, I expect the result to hold