# Axiom, Stacks Project를 Lean으로 기계 검증

> Axiom은 1,600만 줄 분량으로 정형화한 수학 내용을 Lean으로 검증하는 증명에서 재사용할 수 있다고 밝혔다.

Oossa · 2026-11-05 · https://oossa.com/ko/axiom-turns-the-stacks-project-into-machine-checked-lean-code

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 시스템이 만들어낼 수 있는 모든 새로운 수학적 주장이나 소프트웨어가 검증된 것은 아니다.

## 팩트

- Axiom은 2026년 11월 4일 공개했다고 밝혔다.
- Lean 정형화 작업에는 약 1,600만 줄의 코드가 들어 있다.
- Stacks Project는 Johan de Jong이 2005년에 시작했으며, 이후 수학자들의 기여로 확장됐다.
- TechCrunch에 따르면 Axiom은 2026년 3월 Menlo Ventures가 주도한 2억 달러 규모의 시리즈 A 투자를 유치했다.

## 왜 중요한가

대수기하학 연구자들은 이 라이브러리에서 검증된 결과를 재사용해 Lean으로 같은 기초 내용을 다시 구축하는 수고를 덜 수 있다. 이번 공개는 이 참고 자료의 정형화가 검증됐다는 뜻이지, 앞으로 AI가 생성하는 증명이나 코드가 검증 없이도 신뢰할 수 있다는 뜻은 아니다.

## 출처 및 참고 자료

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

최종 업데이트: 2026-11-05