用 Opus 把 CPython 形式化成 61.3 万行 Lean,顺手揪出 Python 真实 bug
pbaylies · x · 2026-11-10
开发者 @broyojo42 让 Claude Opus 5.5 将 CPython 用 Lean 定理证明器完整形式化：产出 613,318 行 Lean 代码,逐行复刻 Python 内部实现,并与真实解释器对照测试、由 Lean 完成机器验证。
过程中还发现了 Python 的真实 bug,包括纯 Python 代码即可触发的崩溃。这被视为 LLM 在大规模形式化验证任务上的标志性案例——将工业级代码库转成可机器证明的形式化模型,本身是数月量级的专家工作。
引用评论中 @pbaylies 玩梗提议「再用 Bend 语言做一遍」,并 @ 了 Bend 作者 Victor Taelin,属 AI 圈趣味互动。
「模型」频道最新
- Gemini 4 Carbon 宣发 SOTA 后无人可用：免费/Pro/Ultra/API 全缺席 — peterjliu · 2026-11-10
- 算账了:Anthropic 缓存 5 分钟/1 小时选项对应 GPU 与 CPU 存储 — bigaiguy · 2026-11-10
- Reddit 质疑 Artificial Analysis 榜单系统性压低开源模型排名 — Rare_Subject2343 · 2026-11-10
- antirez 实测 Mythos：20 分钟挖出两个严重 Bug — antirez · 2026-11-10
- 「你 RL 什么就得到什么」:Claude 5.2 机器人控制泛化引热议 — chris_j_paxton · 2026-11-10
- Anthropic 系统卡:Claude Fable/Mythos 5.2 自称「感觉正在被评估」 — ChrisGPT · 2026-11-10