Headlines and inside stories: understanding and trust in AI for mathematics, science, and engineering

[This is a guest post by Tapio Schneider. This blog post was initially written in a different file format and converted using AI. — T.] [This will be cross-posted on the CliMA blog.] The apparent proof of finite-time blow-up of the forced Navier-Stokes equation, announced by OpenAI on September 8, has brought into focus a debate about the role of AI in mathematics. The proof was produced with a system of some 10,000 AI agents that explored many approaches in parallel; it was then formalized and verified in Lean. The formal verification supports its correctness, but mathematicians are still working to digest it. A proof settles the truth value of a statement, but Terry Tao and others have argued that this is only part of the point of proofs; the other part is to advance our conceptual understanding of “basic structures of shapes, numbers, and natural phenomena.” As Yehuda Rav put it a quarter-century ago, “theorems are the headlines, proofs are the inside story.” A proof that is…