Lean 커널의 Soundness Bug #14576 사후 분석 및 교훈
Postmortem for Kernel Soundness Bug #14576
AI 가 생성한 Collatz 추측 반증 시도가 Lean 커널의 중첩 유도 타입 처리 결함을 드러냈다. 이는 이론적 허점이 아닌 구현 버그로 확인되었으며, nanoda 의 별도 결함과 겹쳐 발견되었다. 우리는 즉시 패치를 배포하고, 독립적인 검증 도구와 커널 불변식을 강화하여 시스템의 신뢰성을 회복했다.
이러한 관심사의 분리 및 격리는 증명 항이 가진 가장 큰 장점 중 하나이다.