OpenAI says AI agents solved major math problem, raising questions for crypto security
OpenAI reports a breakthrough in a fluid-motion problem
On Sept. 8, OpenAI said that about 10,000 concurrent AI agents produced a solution to the Navier-Stokes fluid-motion problem after roughly 88 hours of work.
According to OpenAI, the system generated an analytical proof showing that an initially smooth fluid can develop a singularity in finite time while retaining finite energy. The company says this establishes cases C and D of the Millennium Prize formulation.
OpenAI also said the result was formalized and verified in Lean, a software proof assistant, using GPT-6 Astra in another 17 hours. OpenAI released the proof and its Lean formalization for independent scrutiny.
What this means for smart-contract security
The crypto industry is watching the math result because of formal verification. Formal verification uses mathematical specifications and theorem proving to check whether smart-contract code, the programs that run on blockchains when conditions are met, behaves as intended. Human guidance has often made this process costly and labor-intensive.
Ethereum documentation says formal verification checks whether a contract satisfies the properties developers specified in advance. Poorly written or incomplete specifications can allow vulnerabilities to escape detection even when verification succeeds.
The article argues that stronger AI could reduce the labor required to build proofs while making it more important to decide what the proofs should cover. Access controls, withdrawal conditions, accounting invariants and privileged functions still need to be expressed accurately before a prover can test them.
A mathematician's warning about autonomous AI
Five days before the announcement, mathematician Terence Tao warned about a similar scenario: autonomous AI systems backed by huge computing resources could generate complex Navier-Stokes solutions and formally verify them in systems like Lean, while much of the iterative discovery process stays out of public view.
Tao said failed approaches and intermediate discoveries often produce insights that outlive the final proof. An autonomous system could deliver a correct result without giving humans the same depth of understanding.
What is still unclear
The open question is whether theorem-proving systems that handle research mathematics can adapt to production software and produce proofs that developers and auditors can meaningfully inspect.
The article adds that firms combining automated theorem proving with careful specification design could verify more contracts before deployment and focus human expertise on defining the failures that must never occur.
