AI agents wrote 613,318 lines of Lean that copy Python's internals, tested every piece against real Python, and turned up 418 bug reports along the way.