Don't trust Lean4 alone
Early this week, Open AI announced that they had resolved the Navier-Stokes problem[1] . A few hours later, at a workshop dinner, a frantic inquiring professor came up to my table: "Does anyone here understand Lean? Can it be wrong? Is the solution of Navier-Stokes necessarily true?". I'm choosing to...
Sep 1734