액시옴 스택스 형식화란? 규모·방식·접근·한계

무엇을 형식화했다고 하나

대규모로 만든 코드가 조악하다는 통념에 대한 반례로, 현대 수학의 기반인 스택스 프로젝트 전체를 형식화해 내놓는다.

액시옴은 스택스 프로젝트 전체를 린으로 옮긴 결과물을 2026년 11월 4일 공개한다고 발표했어요. 스택스 프로젝트는 대수기하를 다루는 오픈 백과로, 분량이 7500페이지를 넘어요. 액시옴은 이를 현대 수학을 떠받치는 핵심 인프라로 설명하고, 서로 촘촘히 이어진 구조를 유지한 채 코드 품질을 다듬었다고 했어요.

발표문에서는 이 결과물을 하나의 수학 도시에 비유해요. 통념과 달리 규모를 키워도 코드가 무너지지 않는다는 반례로 내세운 발표예요. 모델 이름, 파라미터 수, 학습 방식, 벤치마크 수치는 함께 공개되지 않았어요.

알려진 규모와 만드는 방식

편집 경위에 따르면 액시옴은 AI 에이전트로 스택스 프로젝트 전체를 린 코드 약 1600만 줄로 바꾸고, 그 결과를 오픈소스로 푼다고 했어요. 확인된 스펙은 여기까지예요. 어떤 에이전트를 몇 개 썼는지, 린 버전은 무엇인지, 증명을 어떻게 검산했는지는 발표에 없어요.

1600만 줄은 원전 7500페이지 이상을 형식 언어로 펼친 규모를 가리켜요. 백과 안의 정의와 정리가 서로 참조하는 연결을 유지했다고 한 점이 이번 발표의 핵심 주장이에요. 줄 수가 곧 증명 완료나 오류 없음을 뜻하는지는 별도로 확인된 바가 없어요.

• 대상

  스택스 프로젝트 전체. 대수기하 오픈 백과이며 7500페이지가 넘어요.

• 산출물

  린 코드 약 1600만 줄. 품질을 다듬고 상호 연결 구조를 보존했다고 해요.

• 수단

  AI 에이전트. 에이전트 구성과 검산 절차는 공개되지 않았어요.

어디부터 볼 수 있나

지금은 짧은 미리보기 영상과 발표만 있어요. 공식 페이지, 다운로드, 공개 빌드는 나오지 않았고, API나 앱, 가중치 공개 여부도 확인되지 않아요. 가격과 사용 한도 역시 발표에 없어요.

오픈소스 공개를 예고했지만 저장소 주소는 아직 없어요. 검색 의도대로 공식 링크를 찾으려면 액시옴이 페이지나 저장소를 열 때까지 기다리는 수밖에 없어요. 따라서 설치, 빌드, 부분 컴파일 같은 하는법은 현재 안내할 수 없어요.

어디에 쓰이고 무엇이 남나

취지에 비추면 이 형식화는 대수기하 문헌을 증명 보조 도구 안에서 검색하고 연결하는 기반이 될 수 있어요. 스택스 프로젝트처럼 정의와 정리가 서로 기대는 글을, 구조를 깨지 않은 채 린으로 옮겼다는 주장이 그 전제예요. 연구자가 바로 불러 쓰는 라이브러리인지는 파일이 공개된 뒤에야 판단할 수 있어요.

비교할 다른 모델의 점수나 가격은 이번 발표에 없어요. 액시옴이 대비한 대상은 특정 제품이 아니라, 규모를 키운 AI 작성 코드는 품질이 낮다는 통념이에요. 독립 검산, 오류율, 유지 주체, 라이선스 문구, 부분만 받는 방법은 모두 열린 질문이에요.