Claude 三个月形式化相对套利定理

Dmitriy Traytel 称，他用 Claude 智能体配合 PIDE MCP，在 Isabelle 中形式化了论文《Relative arbitrage problem under eigenvalue lower bounds》的主定理。三周产出超过 10 万行证明，重构后缩减到约 8.5 万行、12 个 session。 他称整个夏天使用的是每月 100 美元的 Claude Max 5x 订阅（该订阅现已被面向科学家的 Claude Team 计划取代），而 Claude 估算的 API 成本为 7500 美元。当时 PIDE MCP 尚不支持动态处理 session，现在已支持。

AI 根据报道生成 · 1 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。