Ein Entwickler ließ Claude Opus 5.5 CPython in Lean formalisieren: 613.318 Zeilen

Der Entwickler broyojo42 sagt, er habe Claude Opus 5.5 eine Formalisierung von CPython in Lean schreiben lassen: 613.318 Zeilen, die Pythons Interna Zeile für Zeile nachbilden, mit dem echten Interpreter getestet und von Lean geprüft. Dabei habe das Modell echte Fehler in Python gefunden, darunter Abstürze durch gewöhnlichen Python-Code.

Der Beitrag gibt die eigene Darstellung des Autors wieder; bis zum 10. November hatte er auf X 2.066 Punkte. Charlie Marsh von Astral teilte ihn.