앤스로픽 클로드가 358년 난제 페르마의 마지막 정리를 컴퓨터로 완전 검증했어요. 11일간 거의 자율적으로 작업해 1,300만 줄 Lean 코드와 2만9,500개 정리를 만들었죠. AI가 수학 연구의 조수를 넘어 실제 증명 파트너가 될 수 있다는 신호로 읽힙니다.
솔직히 이 소식 보고 좀 놀랐어요. 페르마의 마지막 정리, 다들 한 번쯤은 들어봤을 거예요. "xⁿ+yⁿ=zⁿ을 만족하는 자연수는 n이 3 이상이면 존재하지 않는다"는 그 유명한 명제요. 1637년에 페르마가 책 여백에 "나는 놀라운 증명을 찾았지만 여백이 부족해서 적지 못한다"고 낙서한 뒤로 358년 동안 아무도 완전히 못 풀었던 문제죠. 1994년에야 앤드루 와일스가 완성했는데, 그 증명이 워낙 길고 복잡해서 사실 지금까지도 사람이 한 줄 한 줄 검증하기엔 벅찬 수준이었대요.
그런데 앤스로픽이 지난달, 클로드가 이 증명을 Lean이라는 정리 증명 언어로 완전히 형식화(formalize)했다고 발표했어요. 쉽게 말하면 컴퓨터가 논리적 오류 없이 한 줄씩 검산할 수 있는 형태로 다시 써낸 거예요. 사람이 아니라 기계가 "이 증명, 진짜 맞습니다"라고 확인 도장을 찍어준 셈이죠. 11일 동안 거의 자율적으로 작업했고, 그 과정에서 무려 1,300만 줄의 Lean 코드를 썼고 2만9,500개의 중간 정리를 증명했다고 해요. 숫자만 봐도 감이 잘 안 오는데, 사람 수학자 팀이 몇 년씩 매달릴 분량이라고 하네요.
재밌는 건 접근 방식이에요. 페르마의 정리를 증명하는 방법에는 크게 두 갈래가 있는데, 쿠머의 고전적 방법은 '정규 소수'라는 특정 케이스만 다루고 전체를 커버하지 못해요. 클로드는 와일스와 테일러가 개척한 프레이 곡선·모듈성 리프팅 접근을 그대로 따라갔대요. 지름길을 찾은 게 아니라, 인류가 알고 있는 가장 어려운 정석 루트를 그대로 기계어로 옮긴 셈이죠.
물론 이게 클로드 혼자만의 성과라고 보긴 어려워요. 임페리얼 칼리지 런던의 케빈 버즈워드 교수가 이끄는 Lean 수학 커뮤니티가 수년간 쌓아온 기반 작업 위에서 이뤄진 결과라고 앤스로픽도 명확히 밝히고 있거든요. 사람들이 몇 년간 벽돌을 쌓아뒀고, 클로드가 마지막 몇 달치 작업을 11일 만에 해치운 셈이랄까요. 전체 증명 체인은 anthropics/fermats-last-theorem이라는 깃허브 저장소에 그대로 공개돼 있어서 누구나 직접 뜯어볼 수 있어요.
개인적으로는 이 소식이 벤치마크 점수 경쟁보다 훨씬 의미 있다고 생각해요 🔢. 요즘 AI 뉴스 보면 맨날 "어떤 모델이 어떤 벤치마크에서 몇 점 찍었다"는 얘기뿐인데, 이건 결이 달라요. 수학 증명 검증은 사람이 몇 년씩 매달려도 끝나지 않는 작업이잖아요. 앤스로픽이 리만 가설 관련 연구에도 클로드를 투입했다는 얘기가 나오는 걸 보면, 수학 쪽을 꽤 전략적으로 밀고 있는 것 같기도 하고요.
다만 이게 "AI가 새로운 수학을 발견했다"는 얘기는 아니라는 점은 짚고 넘어가야 할 것 같아요. 어디까지나 이미 증명된 정리를 형식적으로 재작성·검증한 거지, 미해결 난제를 새로 푼 게 아니거든요. 그래도 사람 수학자들에게 몇 년씩 걸리던 검증 작업을, AI가 열흘 남짓 만에 컴퓨터가 확인 가능한 형태로 만들어낸 건 분명 하나의 이정표예요 ✅.
수학 커뮤니티 반응도 궁금해서 좀 찾아봤는데, 반응이 은근 갈려요. "드디어 형식 검증 수학이 실용화 단계에 들어섰다"며 반기는 쪽이 있는가 하면, "커뮤니티가 몇 년간 쌓아둔 인프라 없이는 불가능했던 일인데 클로드 단독 성과처럼 포장됐다"는 지적도 나오더라고요. 둘 다 일리 있는 얘기 같아요. 기반은 사람이 놓았지만, 마지막 스퍼트를 AI가 열흘 만에 해낸 것도 사실이니까요. 다음엔 어떤 정리가 이 리스트에 오를지, 그때는 또 며칠이나 걸릴지 궁금해지네요.
출처