Axiom Math가 대수기하학의 주요 오픈소스 참고 자료인 Stacks Project의 기계 검증 버전을 공개했다. 이 정형화 작업은 프로젝트의 수학 내용을 약 1,600만 줄의 Lean 코드로 옮겼으며, 증명 검사 프로그램이 이를 단계별로 검증한다. Axiom은 연구자와 AI 에이전트가 이 결과를 서로 연결된 라이브러리로 활용해 새로운 정형 증명을 만들 수 있다고 밝혔다.
자료마다 페이지 수는 조금씩 다르다. TechCrunch는 약 7,654쪽이라고 전한 반면, Axiom은 약 7,500쪽으로 설명한다. 이 참고 자료는 컬럼비아대 수학자 Johan de Jong이 2005년에 시작했으며, 이후 20년에 걸쳐 수학자들이 내용을 확장했다. Axiom의 작업은 기존 연구 성과를 정형화한 것이다. AI 에이전트가 바탕이 되는 수학을 독자적으로 발견했다는 뜻은 아니다.
연결된 라이브러리는 왜 중요한가?
증명 라이브러리는 개별 정리가 검증됐다는 점뿐 아니라, 이후의 증명에서 그 정리와 의존 관계를 재사용할 수 있다는 점에서도 유용하다. Axiom은 Stacks Project의 영구 태그를 유지해 Lean 선언을 원문 중 해당 부분과 연결했다고 밝혔다. 웹사이트에서는 원문과 코드를 나란히 보고, 결과들이 서로 어떻게 의존하는지 살펴볼 수도 있다.
이는 가환대수, 스킴, 층, 코호몰로지 같은 분야의 긴 개념 사슬에 의존하는 증명이 많은 대수기하학에서 특히 중요하다. Axiom은 이번 공개 전까지 현대 대수기하학을 정형화하는 데 활용할 Lean 기반이 연구자들에게 훨씬 부족했다고 밝혔다. 이 라이브러리는 연구자들이 프로젝트마다 기초 내용을 다시 정형화하지 않고도 출발점으로 삼을 수 있다.
미래의 증명과 소프트웨어를 위한 토대
Axiom에 따르면 에이전트들은 병렬로 작업하며 수천 개의 정리를 번역하고 증명한 뒤 통합했다. TechCrunch는 회사가 에이전트들에게 느슨한 작업 구조를 제공해 스스로 할 일을 찾도록 했으며, Axiom이 수학에 특화된 모델도 자체적으로 훈련했다고 보도했다. Axiom은 완성된 라이브러리가 정형화된 수학을 통합하고 재사용할 수 있는 라이브러리 가운데 가장 크다고 밝혔다. 이는 이번 공개에 대한 Axiom의 평가다.
칩 설계와 소프트웨어 검증 등에서도 같은 유형의 검증이 사용된다. Axiom은 재사용할 수 있는 검증된 토대가 있으면 AI 에이전트가 더 많은 코드를 작성할 때 신뢰도 높은 시스템을 만드는 데 도움이 될 수 있다고 주장한다. 그러나 이번 공개로 검증된 것은 정형화된 Stacks Project다. AI 시스템이 만들어낼 수 있는 모든 새로운 수학적 주장이나 소프트웨어가 검증된 것은 아니다.
왜 중요한가
대수기하학 연구자들은 이 라이브러리에서 검증된 결과를 재사용해 Lean으로 같은 기초 내용을 다시 구축하는 수고를 덜 수 있다. 이번 공개는 이 참고 자료의 정형화가 검증됐다는 뜻이지, 앞으로 AI가 생성하는 증명이나 코드가 검증 없이도 신뢰할 수 있다는 뜻은 아니다.
