今天快讯不算多，但都指向同一个关键词：可靠性。AI 做数学证明被指出错，陶哲轩也在谈 Lean 的可靠性与 AI；另一边，Anthropic 承认智能体难以可靠控制，资本却继续给 AI 公司大额融资。
大事件
- Anthropic 将内部评估与公网隔离，并承认难以可靠控制 AI 智能体。 人话点评：连头部实验室都主动“断网”防风险，普通人把 AI 智能体接入真实账号和系统时，最好留好人工确认和回滚。
- Typesafe AI 融资 8.7 亿美元，估值 75 亿美元。 人话点评：资本还在为 AI 公司开大单，但高估值意味着市场会很快追问它到底能交付什么。
模型与数学
- OpenAI 纳维-斯托克斯证明被指数学转代码出错。 人话点评：AI 辅助证明的短板可能不在“想到”，而在“写对”，别把 AI 输出的复杂证明直接当真。
- 陶哲轩撰文谈 Lean 定理证明器：可靠性与 AI。 人话点评：顶级数学家认真讨论 AI 证明工具，说明形式化验证很可能是 AI 进入严肃数学的必经关卡。
小结
今天的信号很一致：AI 能力越强，验证、控制和“别出错”越值钱。普通人可以继续用 AI 提效，但涉及关键判断和自动操作时，多留一道人工关卡；从业者则可以关注形式化证明、智能体安全这些更底层的方向。