앤트로픽의 인공지능 모델 클로드가 1995년 앤드루 와일스 경이 증명한 페르마의 마지막 정리를 프로그래밍 언어 Lean으로 옮기는 자동 형식화 작업을 11일 만에 마쳤다. 사람이 몇 년에 걸쳐 하던 엄밀한 논리 검증 작업을 다중 에이전트 기반 자율 워크플로우로 짧은 기간에 해낸 것이다. AI가 복잡한 수학 정리의 완전한 컴퓨터 검증까지 스스로 해내는 단계에 이르렀음을 보여 주는 사례다.

클로드, 페르마의 마지막 정리 형식화 성공

앤트로픽은 클로드 에이전트 수십 개를 묶은 다중 에이전트 워크플로우로 페르마의 마지막 정리 증명을 Lean 언어로 형식화했다고 밝혔다. 1995년 앤드루 와일스 경이 완성한 복잡한 수학 증명 구조를 컴퓨터가 엄밀하게 검증할 수 있는 프로그래밍 언어 코드로 바꾼 것이다.

이 과정에서 인간 연구자는 처음에 목표 정리를 제시하고 시스템을 설정한 뒤, 가끔 우선순위를 정하고 피드백을 주는 정도만 맡았다. 대규모 논리 전개와 증명 코드 작성은 클로드 에이전트들이 11일 동안 스스로 협력하며 해냈다. AI 에이전트가 코드 몇 줄을 만드는 수준이 아니라, 대규모 문제를 자율적으로 풀어내는 시스템으로 쓰일 수 있음을 보여 준 결과다.

앤트로픽의 클로드 에이전트가 11일 만에 페르마의 마지막 정리 증명을 Lean 언어로 형식화했다.

1,300만 줄의 Lean 코드와 중간 정리

이번 프로젝트에서 만들어진 Lean 코드는 약 1,300만 줄이다. 기존 수학 성과를 모아 둔 대표 Lean 라이브러리 Mathlib의 5배가 넘는 규모로, 지금까지 작성된 Lean 기반 형식 증명 가운데 가장 크다.

증명이 얼마나 촘촘한지는 중간 정리 수치에서도 드러난다. 클로드는 최종 증명 과정에서 약 29,500개(세부 집계로는 29,511개)의 중간 정리를 썼고, 형식화 탐색 과정 전체에서는 모두 30,300개의 중간 정리를 증명했다. 이 많은 중간 정리가 하나하나 검증을 거쳐 최종 증명으로 이어졌다.

최종 증명 과정에서 수만 개의 중간 정리가 검증되며 역대 최대 규모의 Lean 형식 증명이 완성되었다.

인간 연구 프로젝트와의 대조

이번 성과는 인간 수학자들이 추진해 온 장기 프로젝트와 뚜렷이 대비된다. 임페리얼 칼리지 런던의 케빈 버자드 교수는 5년간 100만 파운드의 연구비를 지원받아 페르마의 마지막 정리를 Lean으로 형식화하는 프로젝트를 진행하고 있었다.

버자드 교수는 클로드의 증명 결과를 Lean 검증 도구로 직접 확인한 뒤, 수학의 공리 말고는 어떤 가정도 없이 정리를 증명해 낸 특별한 자동 형식화 성과라고 평가했다. 인간 커뮤니티가 몇 년에 걸쳐 하려던 일을 AI가 11일 만에 검증까지 끝낸 셈이다.

5년 프로젝트로 추진되던 인간 수학자의 작업을 AI가 단 11일 만에 자율적으로 달성했다.

AI 자동 형식화가 가져올 변화

이번 성과는 수학 연구뿐 아니라 소프트웨어 엔지니어링 전반에도 시사점이 있다. 다중 에이전트 워크플로우를 쓰면 의존성이 수만 개에 이르는 대규모 논리 체계도 나눠서 효율적으로 처리하고 검증할 수 있다는 것이 확인됐기 때문이다.

소프트웨어 개발자들은 앞으로 이런 에이전트 기반 자동 형식화와 검증 기법을 복잡한 시스템 검증에 응용할 수 있다. 미션 크리티컬한 코드나 보안 프로토콜을 Lean 같은 형식 검증 언어로 정밀하게 검증하는 일이 AI 덕분에 훨씬 널리 쓰이게 될 전망이다.

참고