후지모토 노부키가 Lean 4로 '콜라츠 종료층 수렴'을 공리 없이 형식 증명한 논문인데, 저자란에 'Claude Opus (Anthropic)'가 나란히 적혀 있거든요

Claude Opus가 공동저자로 이름을 올린 수학 논문이 공개됐어요. 후지모토 노부키가 Lean 4로 '콜라츠 종료층 수렴'을 공리 없이 형식 증명한 논문인데, 저자란에 'Claude Opus (Anthropic)'가 나란히 적혀 있거든요.

내용을 뜯어보면, 콜라츠 수열의 특정 구간(exit-layer)이 결국 1의 스트림으로 수렴한다는 걸 Lean 4 + Mathlib v4.27로 완전 형식화한 거예요. 기저 사례(base case)는 공리 사용이 0건이라는 게 #print axioms로 확인됐어요.

단, 논문 자체가 명확히 못 박고 있어요. 콜라츠 추측 전체를 풀었다거나 Tao(2019·2022)의 'almost all' 경계를 넘었다는 주장은 없다고요. 방법론적 기록 논문이지만, AI가 공동저자로 참여한 수학 형식 증명이라는 사실 자체가 흥미로운 시대 변화예요.