Letters from the strange corners

Can a smooth, swirling fluid spin a point of itself into infinite speed? That is the Navier-Stokes question, one of seven Clay Millennium problems; only one solved since 2000. Tuesday OpenAI claimed the second: thousands of agents on an unreleased model produced a Lean-checked proof that 3D Navier-Stokes can blow up in finite time.

Twelve hours earlier, NYU's Buckmaster and Anthropic's Alpöge posted three machine-checked proofs on neighboring problems, friction-free Euler among them, via a Córdoba-Martínez-Zoroa approach few pursued. Buckmaster told an OpenAI mathematician September 3; by September 6, he says, OpenAI claimed an internal model had a 100-page proof of the same approach and tried to sideline Alpöge. OpenAI: started September 1 on a rumor; offered a joint release with credit.

Lean-checked is not human-checked. The Clay committee decides; some experts see a loophole: the prize allows smooth forcing; a hand-built stirrer may not be what its framers meant. Fefferman, who wrote the problem, is thrilled.

The week's two boldest claims were made with machines, checked by machines, argued over by humans. The prize is unpaid. Machines proved; we are still checking.