Một nhà phát triển nhờ Claude Opus 5.5 hình thức hóa CPython bằng Lean, tạo ra 613.318 dòng

Nhà phát triển broyojo42 cho biết họ đã nhờ Claude Opus 5.5 viết bản hình thức hóa CPython bằng Lean: 613.318 dòng sao chép nội bộ Python từng dòng, được kiểm thử với trình thông dịch thực và kiểm chứng bằng Lean. Họ nói rằng trong quá trình này, mô hình đã phát hiện các lỗi thực sự trong Python, bao gồm cả lỗi gây sập chỉ với mã Python thuần.

Bài đăng là lời kể của chính tác giả; tính đến ngày 10 tháng 11, bài đăng có 2.066 điểm trên X. Charlie Marsh của Astral đã chia sẻ bài đăng này.