앤트로픽이 8월 10일 올린 글이에요. 미공개 연구용 클로드가 클로드 코드 세션 두 번 동안 서브에이전트 약 60개를 하루 반 굴려 셸 명령 2,400번과 파이썬 스크립트 수백 개를 돌리고 출력 토큰 3,100만 개를 써서, 리만 제타 함수 영점 가운데 임계선 위에 있다고 증명된 비율의 하한을 41.6%에서 67.2%로 올렸어요 — 프롬프트를 넣은 직원은 수학자가 아니고, 입력은 대부분 '계속해 봐'·'너를 믿어' 였어요. 결과는 Lean으로 옮겨 빠진 단계(sorry) 없이 기계 검사를 통과했다고 저장소에 적혀 있지만, 학술지도 arXiv도 아닌 앤트로픽 서버의 PDF로만 냈고 검토한 사내 수학자 둘은 '심사위원에 가깝다'며 저자에서 빠졌어요.
용어 풀이
- Lean
- 증명을 컴퓨터가 한 단계씩 검사할 수 있게 적는 언어이자 검사 도구
- sorry
- Lean에서 증명을 아직 안 채웠다고 남겨 두는 표시. 이게 하나도 없으면 빠진 단계가 없다는 뜻
- 임계선
- 리만 제타 함수 값이 0이 되는 지점(영점)이 모두 이 세로선 위에 놓인다는 게 리만 가설
- 서브에이전트
- 본 세션이 따로 띄워 일부 작업을 통째로 맡기는 하위 에이전트
운영자 인사이트
에이전트를 하루 반씩 굴려도 되는 조건이 그대로 드러나 있어요 — 맞았는지 기계가 바로 채점해 주고(Lean·수치 검사), 서브에이전트 30개가 헛수고해도 2개만 맞히면 되고, 검증 전담을 13개나 따로 뒀어요. 우리 코드에서 그 채점기는 테스트·타입·빌드라 그게 없는 영역에 같은 방식을 옮기면 실패만 쌓이고, 게다가 이건 미공개 연구용 모델이라 지금 쓰는 클로드 코드로 그대로 재현되는 이야기는 아니에요.
여러 관점으로 보기
- 기계 검사 Lean 4 저장소엔 논문의 정리 A~E가 빠진 단계(sorry) 없이 들어가 있고 표준 공리 셋 말고 더 넣은 공리는 없다고 적혀 있어요 — 아파치 2.0, 별 47개, 열린 이슈 0개, '유지보수 안 함' 연구 산출물이에요. GitHub
- 선행 연구 3분의 2라는 숫자 자체는 2025년 1월 논문에 이미 나와 있어요 — 영점이 임계선을 감싼 좁은 띠 안에 있다는 가정을 깔고서요. 앤트로픽은 클로드가 이 논문에 봄비에리의 2000년 결과를 붙여 41.6% 기록을 넘겼다고 적었어요. arXiv
- 커뮤니티 반응 해커뉴스에선 학술지도 arXiv도 아닌 자체 PDF로만 냈고 저자 이름도 모른다는 지적과, 영점 100%가 임계선 위에 있다고 증명해도 리만 가설보다는 약한 명제라는 지적이 나왔어요. Hacker News