개발자가 Claude Opus 5.5로 CPython을 Lean으로 형식화해 613,318줄을 작성했습니다

개발자 broyojo42는 Claude Opus 5.5를 이용해 CPython을 Lean으로 형식화했다고 밝혔습니다. Python의 내부를 한 줄씩 그대로 옮긴 613,318줄로, 실제 인터프리터와 대조해 테스트하고 Lean으로 검증했습니다. 개발자는 작업 도중 모델이 일반적인 Python 코드만으로도 발생할 수 있는 충돌을 비롯해 Python의 실제 버그를 찾아냈다고 말했습니다.

이 게시물은 작성자가 직접 전한 내용입니다. 11월 10일 기준 X에서 2,066점을 받았습니다. Astral의 Charlie Marsh가 공유했습니다.