用 Claude 和 PIDE MCP 在 Isabelle 中形式化相对套利定理的三个月实践

作者用 Claude 智能体配合 PIDE MCP 在 Isabelle 中形式化了论文《Relative arbitrage problem under eigenvalue lower bounds》的主定理，三周产出超过 10 万行证明，重构后缩减到约 8.5 万行、12 个 session。