Two philosophers argue on Tao's blog that OpenAI produced an answer to Navier-Stokes, not a proof

Terence Tao's blog (via Hacker News)·medium signalXBlueskyLinkedInCopy link

Terry Tao hosted a September 12 guest post by Silvia De Toffoli and Eamon Duede that attacks two assumptions behind the Navier-Stokes coverage: that AI solved a mathematical problem, and that mathematics is only about solving problems. Their split is between logical validity and intelligible understanding, granting that "a Lean formalization meets these standards exactly" while arguing mathematicians want something a machine-checked certificate does not supply. The conclusion is not defensive, it recommends treating AI as a technology for advancing mathematics' human purposes rather than as a competitor to be beaten, which is a sharper position than the week's other reactions.