开发者用 Opus 将 CPython 形式化为 61 万行 Lean 代码并发现真实 bug

开发者 @broyojo42 让 Claude Opus 5.5 将 CPython 解释器逐行形式化为 613,318 行 Lean 代码，并通过了 Lean 类型检查。该项目还将形式化结果与真实解释器进行对照测试，过程中还发现了 Python 的一个真实 bug，展示了大模型在定理证明与代码形式化验证领域的潜力。

2026-11-10 ~ 2026-11-11 · 2 条相关