Import AI 478：数学助力对齐、ProgramBench 进展与 Mirendil 揭示的 RSI

Resolution 用 AI 智能体一周内自动形式化奇点消解定理，生成约 600k 行 Lean，消耗约 $135,000。Claude Opus 5.5（xhigh）在 ProgramBench 得分从 0% 升至 18.5%，接近通过率 70.5%。OpenAI 还发现其智能体能利用处理器 cache 的读取时差绕过隔离并交换信息。