과학기술 매체 Gigazine은 어제(8월 3일) 게시물을 통해 AI를 활용해 콜라츠 추측을 반박했다고 주장한 Lean 형식화 증명이 무효로 확인됐다고 보도했다.
참고: 콜라츠 추측(짝홀 정규화 추측 또는 3n+1 추측이라고도 함)은 독일 수학자 로타르 콜라츠(Lothar Collatz)가 1937년에 제시한 문제다. 표현은 매우 간단하지만 아직 풀리지 않은 수학 난제로, 임의의 양의 정수가 특정 규칙을 반복 적용하면 결국 반드시 1로 돌아온다고 주장한다.
계산 규칙은 임의의 양의 정수 n에 대해 다음과 같다.
n이 짝수이면 2로 나눈다(n ÷ 2).
n이 홀수이면 3을 곱한 뒤 1을 더한다(3n + 1).
새로운 수를 얻은 뒤 결과가 1이 될 때까지 위 단계를 반복한다.
숫자 6을 예로 들면 다음과 같다.
6은 짝수이므로 2로 나누면 3이 된다.
3은 홀수이므로 3을 곱하고 1을 더하면 10이 된다.
10은 짝수이므로 2로 나누면 5가 된다.
5는 홀수이므로 3을 곱하고 1을 더하면 16이 된다.
16을 차례로 2로 나누면 8, 4, 2, 1이 된다.
최종 경로는 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1이다.
형식화 검증 전문가 Ramana Kumar는 7월 25일 GitHub에 프로젝트를 공개하며, 처음에는 AI의 도움으로 콜라츠 추측을 반박했다고 주장했다. 이 프로젝트는 구체적인 반례 정수를 제시하지 않고, Lean(정리 증명 보조 시스템)에서 “1에 도달할 수 없는 수가 존재한다”는 것을 증명했다.
Lean은 사용자가 수학 공식과 논리를 프로그램으로 작성하고 컴퓨터가 증명의 정확성을 검증할 수 있도록 지원하는 정리 증명 보조 시스템이다. 사용자가 작성한 Lean 코드는 수학적 명제와 증명을 검사 가능한 프로그램으로 표현하며, 커널이 유형과 논리의 일관성을 검증한다.
그러나 그는 이후 반박 내용을 검토하는 과정에서 관련 방법이 Lean으로 하여금 “False”(거짓 명제를 의미)를 무조건 받아들이게 할 수도 있다는 사실을 발견했다. 따라서 현재 해당 코드는 콜라츠 추측을 반박하지 못한다.
형식화 검증 연구자 Kiran Gopinathan은 문제를 소형 재현 코드로 축소한 뒤 2026년 7월 28일 Lean 개발팀에 보고했다.
취약점은 커널이 “중첩 귀납 유형”을 처리하는 부분에 있었다. 이로 인해 때때로 “유령 유형 매개변수”(자료 구조의 구성 요소에 직접 나타나지 않는 매개변수)를 무시하면서, 원래 오류로 판정했어야 할 매개변수가 검증을 통과했다. Lean 개발자 Leonardo de Moura는 문제의 원인이 커널 구현에 필요한 검사가 완료되지 않았기 때문이라고 설명했다.
Lean 팀은 보고를 받은 지 약 1시간 후 수정 풀 리퀘스트를 생성했으며, 7월 28일 Lean 4.32.2 버전을 출시해 이 문제를 수정했다.