앤트로픽이 9월 4일 클로드 페이블 5.1급 사내 연구 모델로 페르마의 마지막 정리를 린 4에서 형식화했다고 발표했어요. 11일 동안 출력 토큰 60억 개를 써서 정리 29,511개를 증명했고, 사람이 넣은 수학은 '스킴으로서의 야코비안이 우선순위 높아 보인다' 같은 가끔의 큰 방향 지시뿐이었대요. 공개된 저장소는 아파치 2.0에 커밋 한 개짜리 연구 산출물인데, sorry·추가 공리·native_decide 가 하나라도 섞이면 빌드가 깨지는 검사를 걸어 뒀고, 5년째 같은 일을 해 온 케빈 버자드가 직접 받아 돌려 통과를 확인했어요.
용어 풀이
- 린(Lean)
- 증명을 기계가 검사할 수 있게 적는 프로그래밍 언어 겸 증명 보조 도구
- mathlib
- 린으로 쌓아 온 공식 수학 라이브러리
- sorry
- 린에서 증명을 비워 둔 자리를 표시하는 말. 남아 있으면 그 부분은 아직 증명되지 않은 것
- native_decide
- 린에서 판정을 컴파일된 코드 실행으로 대신하는 명령. 믿어야 할 범위가 넓어져 엄격한 증명에선 금지하기도 함
운영자 인사이트
검증기가 맞고 틀림을 바로 채점해 주는 영역에선 에이전트 떼가 사람 개입 거의 없이 11일을 이어 갈 수 있다는 증거라, 타입 검사·테스트·정적 분석이 촘촘한 코드베이스일수록 맡길 수 있는 범위가 넓어져요. 다만 결과물은 1,340만 줄에 mathlib 의 20배 시간이 걸려 빌드되고 이름도 기계가 붙인 것이라, 통과하는 코드와 사람이 읽고 이어받을 코드는 여전히 다른 물건이에요.
여러 관점으로 보기
- 앤트로픽 발표 (만든 쪽) 11일·출력 토큰 60억 개로 정리 29,500여 개를 증명했고, 실패한 시도들이 최종 증명에서 틀에 박힌 부분을 뺀 줄의 7%를 남겼다고 밝혔어요. Anthropic
- 저장소 실물 (주장과 대조) 미완성 표시 sorry 가 0개이고 린 기본 공리 셋만 쓰지만, 사람이 쓴 기존 프로젝트에서 가져온 파일이 106개(대부분 임페리얼 칼리지 쪽)라고 저장소가 직접 밝혀 뒀고 '유지보수도 기여도 받지 않는 연구 산출물'이라고 적혀 있어요. GitHub
- 먼저 하던 수학자의 평가 케빈 버자드는 직접 받아 돌려 통과를 확인하면서도 '수학적으로 알려 주는 건 사실상 없다'고 적었고, 주 논증이 p≥17 에서만 통하고 빌드가 mathlib 의 20배 걸린다는 점을 함께 짚었어요. Xena Project