Resolution展示数学形式化进展

发生了什么

据Import AI报道，AI安全初创公司Resolution通过自动形式化数学陈述，完成了奇点消解（Resolution of Singularities）的自动形式化工作。该项目耗时约一周，消耗约1000亿输入token（90%为缓存读取）及约3亿输出token，总计花费约13.5万美元，生成约60万行Lean代码。此外，Claude Opus 5.5在ProgramBench基准测试中达到18.5%的解决率，较该基准发布时所有模型0%的得分有显著提升。