Разработчик поручил Claude Opus 5.5 формализовать CPython на Lean: 613 318 строк

Разработчик broyojo42 утверждает, что поручил Claude Opus 5.5 формализовать CPython на Lean: получилось 613 318 строк, построчно копирующих внутреннее устройство Python, протестированных на настоящем интерпретаторе и проверенных Lean. По его словам, в ходе работы модель обнаружила реальные ошибки в Python, в том числе приводящие к сбоям при выполнении обычного кода на Python.

Это личный рассказ автора поста; к 10 ноября он набрал 2 066 баллов на X. Charlie Marsh из Astral поделился им.