Formalizing CPython

Researchers used AI agents to write 613,318 lines of code in Lean that mirrored Python's internals, line by line, and checked every proof against the real Python code. This effort uncovered 418 bug reports in Python. The project aimed to formalize Python's specification by writing precise mathematical proofs about its functions, which forced the researchers to clarify the code's behavior in edge cases. The AI agents successfully wrote proofs, but the initial results were not as useful as expected, with only a small fraction of the proofs holding up to scrutiny, highlighting the challenge of creating meaningful proofs for complex codebases like CPython.