OpenAI 表示，AI 代理生成了一个 Navier-Stokes 证明，并在 Lean 中验证了它。 对于智能合约，自动化证明可以减少验证工作量。但它们只检查指定的规则。遗漏的提款保护措施仍可能导致资金暴露。