The part of Navier-Stokes no one is talking about

John D. Cook 聚焦 OpenAI 同步发布 Lean 4 形式化证明这一动作，并引用旧估算：本科教材每页形式化约需 40 小时。文章称 166 页研究论文的 Lean 验证实际用了 17 小时，折算为四个数量级的成本下降，提示形式化方法可能从昂贵审计变成常规工具。