Un développeur a fait formaliser CPython en Lean par Claude Opus 5.5, en 613 318 lignes

Le développeur broyojo42 affirme avoir demandé à Claude Opus 5.5 de formaliser CPython en Lean : 613 318 lignes qui reproduisent les mécanismes internes de Python ligne par ligne, testées avec l’interpréteur réel et vérifiées par Lean. Il affirme qu’au cours du travail, le modèle a trouvé de véritables bugs dans Python, notamment des plantages provoqués par du code Python ordinaire.

Il s’agit du témoignage de l’auteur du post, qui avait recueilli 2 066 points sur X au 10 novembre. Charlie Marsh, d’Astral, l’a partagé.