有人让 Opus 5.5 把 CPython 逐行抄成 Lean 形式化证明，写了 61 万多行 Lean、通过 4071 个函数、攒了 18898 条定理，顺手挖出 418 个 Python 自身的 bug，其中约 55 个能用普通 Python 代码就把解释器搞崩溃或破坏内存。项目只完成了 CPython 的 16%，但方法本身通用：先抄代码、再用 5 万组输入对照实测、最后让另一 agent 独立复核才算数。
来源： https://broyojo.com/python-formalization/
|
