A smarter plan instead of a faster computer?

What is being checked

This illustrates a hope: new ways of computing might change more than faster computers. It is not a demonstrated application of the current research.

On 26 October, OpenAI announced results in computer science, mathematics and physics. A claimed refutation of the Exponential Time Hypothesis has prompted particular discussion. Roughly speaking, it concerns how sharply the computation required for certain difficult problems must grow in the worst case.

The public examination blog now reports early attempts to run the formal proofs with the Lean proof checker on other computers. A post dated 30 October collects these replications. This is a concrete checking step, not yet a complete expert assessment of the assumptions and consequences.

The experts involved explicitly stated that their participation was not certification of the claim. The announcement therefore does not mean our delivery vans will get better routes tomorrow. What matters is the path from a generated proof to a result that others can reconstruct and understand.