एक डेवलपर ने Claude Opus 5.5 से Lean में CPython को औपचारिक रूप से निर्दिष्ट करवाया—613,318 पंक्तियों में

डेवलपर broyojo42 का कहना है कि उन्होंने Claude Opus 5.5 से Lean में CPython का औपचारिक रूपांतरण लिखवाया: 613,318 पंक्तियाँ, जिनमें Python की आंतरिक कार्यप्रणाली को पंक्ति-दर-पंक्ति हूबहू उतारा गया है। इसे असली इंटरप्रेटर के साथ जाँचा गया और Lean से सत्यापित किया गया। उनका कहना है कि इस दौरान मॉडल को Python में असली बग मिले, जिनमें साधारण Python कोड से होने वाले क्रैश भी शामिल हैं।

यह पोस्ट लेखक का अपना विवरण है; 10 नवंबर तक इसे X पर 2,066 पॉइंट मिले थे। Astral के Charlie Marsh ने इसे साझा किया।