Seorang developer meminta Claude Opus 5.5 memformalkan CPython dalam Lean, dengan 613.318 baris

Developer broyojo42 mengatakan bahwa mereka meminta Claude Opus 5.5 menulis formalisasi CPython dalam Lean: 613.318 baris yang menyalin internal Python baris demi baris, diuji terhadap interpreter sebenarnya dan diperiksa oleh Lean. Mereka mengatakan bahwa dalam prosesnya, model menemukan bug nyata di Python, termasuk yang menyebabkan crash hanya dengan kode Python biasa.

Unggahan ini merupakan penuturan penulis sendiri; unggahan tersebut mendapat 2.066 poin di X per 10 November. Charlie Marsh dari Astral membagikannya.