앤스로픽(Anthropic)의 인공지능(AI) 클로드(Claude)가 350년 난제였던 '페르마의 마지막 정리' 증명을 단 11일 만에 컴퓨터로 검증 가능한 형태로 형식화하는 데 성공했습니다. 이는 AI가 새로운 수학적 증명을 발견한 것이 아니라, 앤드루 와일즈(Andrew Wiles)가 1995년에 발표한 기존 증명을 Lean이라는 형식 증명 보조기(proof assistant) 언어로 옮겨 처음부터 끝까지 컴퓨터가 검증할 수 있도록 만든 것입니다. 이 성과는 수천 쪽에 달하는 복잡한 수학 논문의 오류 탐지 및 검토 부담을 획기적으로 줄일 가능성을 보여줍니다.
이번 형식화 작업에는 수십 개의 클로드 에이전트가 'Prove2Me'라는 협업 플랫폼을 통해 정리 의존성 그래프를 공유하며 진행되었습니다. 이들은 총 3만 300개의 정리를 증명했고, 최종 결과물에는 2만 9,500개가 사용되었습니다. 그 결과, Lean 코드 1,300만 줄이라는 방대한 분량이 생성되었는데, 이는 기존 수학 라이브러리인 Mathlib보다 5배 이상 큰 규모입니다. 앤스로픽은 약 60억 개의 출력 토큰과 클로드 페이블 5.1(Claude Fable 5.1) 수준의 내부 범용 연구 모델을 활용했으며, 형식수학자 케빈 버자드(Kevin Buzzard)도 직접 코드를 컴파일하여 검증 결과를 확인했습니다.
이러한 자동 형식화는 수학 연구 방식에 중대한 변화를 가져올 잠재력을 지닙니다. 복잡한 수학 증명은 한 단계의 오류가 전체를 무너뜨릴 수 있어, 검토에 수개월에서 수년이 걸리기도 합니다. 과거 토머스 헤일즈(Thomas Hales)의 '케플러 추측' 증명은 12명의 심사자가 4년간 검토하고도 99% 확신에 그쳤으며, 그리고리 페렐만(Grigori Perelman)의 '푸앵카레 추측' 증명은 수용까지 4년이 걸렸습니다. AI를 통한 형식 검증은 이러한 인간 검토의 한계를 보완하고, 오래된 논문의 논리적 공백을 찾거나 새로운 논문의 심사 부담을 줄이는 데 기여할 수 있습니다. 궁극적으로는 AI가 생성하는 방대한 수학적 결과의 신뢰성을 확보하고, 인간 수학자가 더 창의적인 연구에 집중할 수 있는 환경을 조성할 것으로 기대됩니다.