중국계 인공지능 스타트업이 650명 20년간 쓴 수학 백과를 검증 가능한 코드로 전환

인공지능 수학 스타트업 액시엄매스는 11월 4일 약 1,575만 줄의 코드를 공개하며, 20년간 650명 이상이 축적한 대수기하학 참고서 스택스 프로젝트를 컴퓨터가 단계별로 검증할 수 있는 린 형식화 체계로 바꿨다고 밝혔다. 스택스 프로젝트는 컬럼비아대 수학자 존 데 용이 2005년부터 시작한 오픈소스형 참고서로, 116장, 7,600여 쪽, 2만 개 이상의 정의와 보조정리, 정리로 구성돼 대수기하학의 위키백과로 불린다. 각 항목에는 고정된 4자 라벨이 부여되고, 긴 증명이 짧은 보조정리들의 의존망으로 짜여 있어 자동 형식화에 유리하다는 평가를 받아왔다. 액시엄매스는 이 프로젝트를 린의 공동 수학 라이브러리인 매틀립 위에 다시 구현했다. 조직은 전체 설계를 담당하는 에이전트, 핵심 정의를 작성하는 에이전트, 개별 증명을 수행하는 에이전트로 나뉘어 인간 작업자가 지시를 내리는 방식으로 움직였다. 이 과정에서 원서에 담긴 수십 개의 명제가 국소적으로 수정돼야 함을 드러냈고, 일부에서는 반례도 제시했다. 공개된 코드에는 매틀립에 이미 포함된 라벨과 린에 적합하지 않은 라벨이 별도로 표시됐으며, 예제와 연습문제, 주석은 외부 기여자가 진행할 과제로 남겼다. 모든 항목은 린 코드와 의존관계로 연결돼 논리적 추적을 가능하게 한다. 이번 작업은 2025년 설립된 액시엄매스가 이미 완료한 소수 간격 246 정리와 유한단군 분류 정리 형식화 흐름의 연장선이다. 다만 소수 간격과 유한단군 분류가 완결된 정리의 개별적 검증에 가까웠다면, 스택스 프로젝트는 수학적 배경을 지속 갱신하고 다른 연구와 에이전트가 재사용할 수 있는 공용 기반을 만드는 데 초점을 맞췄다. 액시엄매스는 사람이 승인한 핵심층과 미검증 전선층을 분리하고, 외부 기여자가 전선층 코드를 검토해 핵심층으로 옮기는 체계를 유지한다. 다만 스택스 프로젝트 운영진 쪽은 생성형 인공지능이 만든 코드를 원류 저장소에 바로 통합하지 말 것을 권고해, 이번 형식화는 액시엄매스 저장소에서 별도 관리된다. 전문가들은 린 검산기가 각 단계의 논리적 적법성만 보증할 뿐, 원서의 의도가 코드에 충실히 담겼는지는 판별하지 못한다고 본다. 따라서 대규모 자동 형식화의 확산에는 인간 검토와 수학적 합의 형성이 병행돼야 한다는 지적이 나온다. 최근 린 공동체에서도 인공지능이 방대한 수학 형식화를 가능하게 했다는 평가와 함께, 연구에 실제로 쓰이지 않으면 형식화 성과의 가치도 제한될 수 있다는 우려가 제기됐다. 그럼에도 검증된 수학 지식이 누적될수록 인간 연구자와 인공지능 모두 기존 결과를 검색, 결합, 확장하기 쉬워져 대규모 형식화가 일회성 시연이 아니라 지속 가능한 인프라로 성장할 수 있다는 기대도 커지고 있다.