Een ontwikkelaar liet Claude Opus 5.5 CPython formaliseren in Lean: 613.318 regels

De ontwikkelaar broyojo42 zegt dat die Claude Opus 5.5 CPython liet formaliseren in Lean: 613.318 regels die de interne werking van Python regel voor regel kopiëren, getest tegen de echte interpreter en gecontroleerd door Lean. Volgens de ontwikkelaar ontdekte het model onderweg echte bugs in Python, waaronder crashes door gewone Python-code.

Dit is het eigen verslag van de auteur; het bericht had op 10 november 2.066 punten op X. Charlie Marsh van Astral deelde het.