Import AI 478：数学助力 AI 对齐、ProgramBench 与 Mirendil 展示递归自我改进的面貌

Import AI 478 汇总 AI 研究进展，重点讨论数学形式化、程序重建基准、智能体安全和 AI 辅助模型训练。Resolution 用智能体将奇点消解定理形式化，耗时约一周，花费约 $135,000，并生成约 600k 行 Lean；Claude Opus 5.5 在 ProgramBench 上取得 18.5% 完全通过率和 70.5% 接近通过率。