Bir geliştirici, Claude Opus 5.5'e CPython'ı Lean'de 613.318 satırla biçimsel olarak tanımlattı

Geliştirici broyojo42, Claude Opus 5.5'e CPython'ın Lean'de biçimsel bir tanımını yazdırdığını söylüyor: Python'ın iç işleyişini satır satır kopyalayan, gerçek yorumlayıcıya karşı test edilmiş ve Lean tarafından denetlenmiş 613.318 satır. Süreç boyunca modelin, yalnızca sıradan Python koduyla tetiklenebilen çökmeler de dahil olmak üzere Python'da gerçek hatalar bulduğunu belirtiyor.

Gönderi, yazarın kendi anlatımıdır; 10 Kasım itibarıyla X'te 2.066 puan almıştı. Astral'dan Charlie Marsh gönderiyi paylaştı.