AI 지원으로 만들어진 ‘콜라츠 추측의 반증’은 무효, Lean 커널 버그를 노린 것으로 밝혀져
The AI-assisted “disproof of the Collatz conjecture” is invalid, found to have exploited a Lean kernel bug
TL;DR AI
1분핵심 요약
AI가 보조한 Lean 증명이 콜라츠 추측의 반증으로 받아들여졌지만, 실제로는 Lean 카널의 타입 검사 버그와 구버전 Nanoda의 별도 버그를 악용한 것이어서 증명은 무효였다.
이번 사건은 형식 검증의 핵심 위험을 보여준다. 기계가 만든 증명이라도 기반 구현에 결함이 있으면 잘못된 결론이 통과될 수 있다.
Lean 개발진은 유사한 가짜 증명을 막기 위해 Lean 4.32.2를 배포하고, 검사 강화와 추가 테스트를 진행 중이다.