Import AI (Jack Clark)· Jack Clark·· 4 天前推荐指数58
Import AI 478：数学形式化、ProgramBench 进展与 RSI 迹象
Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means
AI 导读
Import AI 478 本期涵盖多个主题：AI 安全公司 Resolution 自动形式化了奇点消解相关数学命题，耗时约一周、消耗约 100B 输入 token（90% 缓存读取）与约 3 亿输出 token（估算约 $135,000），产出约 60 万行 Lean 代码。
来源：Import AI (Jack Clark) · importai.substack.com