OpenAI says AI agents produced a Navier-Stokes proof and verified it in Lean. For smart contracts, automated proofs could cut verification work. But they only check specified rules. An omitted withdrawal safeguard can still leave funds exposed. (CryptoSlate)