Import AI· Jack Clark·· 1 天前AI 评分48
Import AI 478：用数学助力对齐、ProgramBench、Mirendil 展示什么是 RSI
Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means
AI 导读
AI 安全公司 Resolution 自动形式化了统计学习理论相关数学命题（奇点消解），用编排智能体协调多个智能体写 Lean 和纸笔推导，耗时约一周、花费约 135,000 美元 token、产出约 60 万行 Lean 代码。
来源：Import AI · importai.substack.com