開発者、Claude Opus 5.5にLeanでCPythonを形式化させる――61万3,318行

開発者のbroyojo42によると、Claude Opus 5.5にLeanでCPythonの形式化を書かせたという。Pythonの内部実装を1行ずつ再現したLeanコードは61万3,318行に及び、実際のインタープリターとのテストとLeanによる検証を行った。作業の過程で、モデルは通常のPythonコードでクラッシュを引き起こすものなど、Pythonの実際のバグを発見したという。

この投稿は著者本人による報告で、11月10日時点でX上で2,066ポイントを獲得していた。AstralのCharlie Marshも共有した。