Deweloper wykorzystał Claude Opus 5.5 do sformalizowania CPythona w Lean: 613 318 wierszy

Deweloper broyojo42 twierdzi, że kazał Claude Opus 5.5 napisać formalizację CPythona w Lean: 613 318 wierszy, które odwzorowują wewnętrzne mechanizmy Pythona linijka po linijce, są testowane z użyciem prawdziwego interpretera i weryfikowane przez Lean. Twierdzi, że po drodze model znalazł prawdziwe błędy w Pythonie, w tym takie, które powodują awarie przy użyciu zwykłego kodu w Pythonie.

To relacja samego autora; do 10 listopada wpis zdobył 2066 punktów na X. Udostępnił go Charlie Marsh z Astral.