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…
In the News: November 10, 2026 (Midday)
Agents modelled 15.7% of CPython in Lean and found 418 bugs; the authors found many early proofs were correct but checked nothing.
Midday edition
Machine-readable
Download Markdown