Agents modelled 15.7% of CPython in Lean, found 418 bugs, and showed that correct proofs can check nothing

Andrews and Zhang pointed Opus 5.5 at CPython 3.15.2 and had agents copy its functions into Lean line by line. Each function goes through four steps: copy the source, test the copy against real Python on at least 50,000 inputs, prove or refute properties, and pass review by a second agent that did not write it. By their count, 4,071 of 26,004 in-scope functions (15.7%) have passed that review since the project started on October 29, giving 613,318 lines of Lean in 1,539 files and 18,898 theorems and lemmas checked on every build. They rate most of the 418 bug reports as small and say about 55 can crash the interpreter or corrupt memory from ordinary Python code.

Their first pass asked for breadth, at least one proof per function. A separate review then found that fewer than half of the functions it checked held up, and in one file only 21%. "The proofs were all correct. They just didn't say anything useful." The reviewer now asks one question of every proof: "could a broken version of the function pass it too?" Every accepted statement is also run against real Python, which caught valid proofs about a wrong copy, such as a JSON encoder model that assumed memory requests always succeed.

The repository publishes the instructions the agents worked from (AGENTS.md for the modelling agents, REVIEW_PROMPT.md for the reviewers) and one bug record per finding. Its README says each record carries a reproducer that prints REPRODUCED on 3.15.2; we have not run them. The authors say the reports not already on CPython's tracker are being filed with the project. The post had 118 points and 54 comments on Hacker News at about 13:05 EST on November 10.

Why it matters: A checker accepting agent output does not mean the output tests anything, and this project measured that gap on its own work. The reviewer's question about a broken version, and the rule that a false statement keeps its counterexample instead of being weakened until it proves, carry over to any loop where agents write both the code and the checks on it.