요약
AI 수학 기업 액시엄이 대수기하학 참고서 Stacks Project 전체를 Lean으로 형식화해 공개했습니다.
Stacks Project는 컬럼비아대 수학자 요한 더용이 2005년 시작한 약 7,500쪽 분량의 공개 참고서입니다. 액시엄은 AI 에이전트 무리를 동원해 이를 Lean 코드 약 1,600만 줄로 옮겼다고 밝혔습니다.
왜 중요한가
- 연구자와 AI 에이전트가 스킴 같은 기초 개념을 처음부터 다시 만들지 않고 바로 가져다 쓸 수 있습니다.
- 액시엄은 AI가 사람이 손으로 확인하는 속도보다 빨리 증명을 내놓는 만큼 형식 검증(컴퓨터로 증명을 검사하는 일)이 필수가 된다고 봤습니다.
- 잘 정리된 문헌으로 꼽히는 원문에서도 빈틈이 드러나, 형식화가 기존 문헌을 바로잡는 데 쓰일 수 있음을 보였습니다.
핵심 내용
- 가설이 빠졌거나 양의 표수 같은 특수한 경우에 성립하지 않는 명제 수십 개를 찾아 반례와 수정안을 만들었습니다.
- 역할을 나눈 에이전트들이 명제 번역, Mathlib(Lean의 수학 라이브러리) 검색, 증명 작성을 병렬로 맡았습니다.
- 명제가 원문과 같은 뜻인지는 에이전트끼리의 교차 감사와 원문 대조로 확인하고, 핵심 정의와 주요 정리는 따로 점검했습니다.
- 각 Lean 선언에 원문의 항목 번호(Stacks 태그)를 달고, 원문과 코드를 나란히 보는 사이트도 열었습니다.
- 더용이 AI가 만든 기여를 당분간 원래 저장소에 보내지 말라고 요청해, 수정 사항은 액시엄의 별도 저장소에만 둡니다.
HN 반응
- 일부 이용자는 Stacks Project가 원래 자연어로 쓴 Lean처럼 체계적이라 형식화에 알맞다고 반기며, 찾아낸 빈틈의 내용을 더 알고 싶어 했습니다.
- 반면 원래 프로젝트가 최근 "당분간 AI는 받지 않는다"는 글을 올린 점을 들며, 사람이 이해하지 못하는 증명만 쌓인다는 우려와 발표문이 AI 문체라는 비판도 나왔습니다.
유한 단순군 분류(CFSG)의 형식화가 발표된 뒤, 저는 곧바로 “Stacks Project를 형식화하려 들면 어떻게 될까?” 하는 생각이 들었습니다. 이쪽도 분량이 아주 방대하지만 CFSG와는 정반대입니다. CFSG가 하나의 큰 정리를 증명하는 데 보탬이 되는, 정리가 잘 안 된 결과들의 모음이라면, Stacks Project는 넓은 분야를 아우르는 결과들을 꼼꼼하게 짜 맞춘 모음입니다.
Stacks Project는 (적어도 LLM 이전 시대에는) 수학을 어떻게 해야 하는지 보여 주는 본보기였습니다. 대수기하학에는 정리가 제대로 안 된 기초 결과가 많았고, 그 결과들은 그 자체를 위해서라기보다 이 분야의 문제를 풀기 위해 만들어진 것이었습니다. 아이서 요한 더 용(Aise Johan de Jong) 한 사람이 이를 바로잡겠다며 나섰고, 모든 결과의 증명을 체계적으로 적어 내는 프로젝트를 꾸렸습니다. 그 뒤로 줄곧 그가 프로젝트를 이끌고 있고, 물론 기여자는 여럿입니다. 전체 분량은 수천 쪽에 이릅니다.
기존 결과에서 어떤 빈틈을 찾아냈고 그것을 어떻게 메웠는지 더 듣고 싶습니다.
저는 증명이 싸진 시대에는 이 방식이 맞지 않다고 봅니다. 타입 이론이라는 구속복 때문에, 여러 분야에 걸쳐 증명을 공유하는 일은 대부분의 사람이 읽고 소화하기에 고통스럽습니다. AI가 있으면 이론을 특화하는 일이 훨씬 쉽습니다. 넓고 얕은 이론 위에 쌓아 올리는 인지적 비용은 치를 만한 가치가 없습니다. AI를 따라잡을 희망이 조금이라도 있으려면, 우리는 오히려 뇌에서 가장 큰 부위, 곧 시각 피질에 더 잘 호소하는 방향으로 가야 합니다.
시각 피질은 뇌에서 가장 큰 부위가 아니에요.
어... ‘특화된 이론’이라는 게 결국 덜 일반적인 결과를 뜻하는 거잖아요. 그런 구속복은 수학의 정신에 완전히 어긋나요.
Lean 증명이 얼마나 많이 타입 사이의 변환 작업일 뿐인지 보신 적 있어요?
공교롭게도 (오늘 기준으로) 원조 Stacks Project의 가장 최근 블로그 글이 2026년 10월 21일 자 “21 Oct 2026: No AI for now”라는 게 좀 아이러니합니다.
아주 가까운 제 친구가 대수기하학자인데, 수학 분야의 AI 발전이 전부 그를 좀 많이 우울하게 만들고 있습니다. 솔직히 저도 마찬가지고요!
어느 정도는 AI로 이런 작업을 하고 싶은 마음이 이해가 됩니다. 하지만 사람이 이해하기 어렵거나 불가능한 “지식”을 (대규모로든 아니든) 생산하는 것에는 점점 회의가 듭니다.
AI 시대 수학의 병목은 여전히 사람의 이해입니다. 아무리 새로운 걸 많이 증명해 내도, 뭔가를 이해하려면 결국 옛날 방식대로 해야 합니다. AI가 조금은 도울 수 있겠지만, 문제를 직접 풀고 증명을 따라가 보지 않으면 크게 나아갈 수 없습니다. 결국 우리 정신은 그런 식으로 한계가 있습니다.
AI 이전의 수학 발전 속도는 대체로 인간이 이해를 소화하는 방식에 맞아 있었다고 생각합니다. 그런데 AI가 들어온 지금은 수학이 훨씬 빠르게 나아가면서 우리의 이해 능력을 앞질러 버릴 겁니다.
더 많은 수학자가 이론적으로는 언젠가 그것을 훑어볼 수 있겠지요. 하지만 발전 과정 자체가 의욕을 꺾고, 그래서 역설적으로 이 새로운 AI 시대의 수학은 많은 사람에게 훨씬 덜 흥미로워집니다.
장담하는데, 처음의 “이만큼이나 증명할 수 있다니” 하는 단계가 지나면 AI를 쓰는 이점은 빠르게 줄어들 겁니다.
좋아요, 이건 정말 쓸모 있는 AI 형식화네요. 그런데 Stacks Project는 사실상 자연어로 쓴 Lean이나 다름없으니, 품질이 높은 것도 납득이 가요.
수학자들이 왜 기업 제품 위에 뭔가를 쌓으려 하겠어요? 자유롭고 열린 학술 연구의 원칙에 어긋나는데요.
관련 글입니다.
https://news.ycombinator.com/item?id=40025362
정리의 가설을 형식화한 것이 맞는지 어떻게 검증했는지 나와 있나요? (아직 읽어 보지 못해서 죄송합니다.)
설명문부터 AI 슬롭이라는 사실이 결과물에 대한 신뢰를 떨어뜨리네요.
슬롭 문장, 당신의 HN 피드로 직배송
액시엄(Axiom)이 2억 6,400만 달러를 투자받아서 AI로 만든 이 어마어마한 Lean 증명을 공개했는데, 설명에 AI 말투가 좀 들어갔다고 투덜대는 거예요? 도메인 이름에도 AI가 들어 있는데요. 지금 뭐 하시는 거예요?
그만한 돈이 있으면 글쓰기 수업 들은 사람 한 명쯤은 고용할 수 있을 텐데요.
AI를 쓴다고 해서 형편없이 써도 되는 건 아니에요. 늘 그걸 핑계로 대긴 하지만, 그래선 안 되죠.
뭐가 나쁘다는 거죠? 막연한 주장엔 알맹이가 없어요.
AI 특유의 표현 하나는 여기에 적었습니다. https://news.ycombinator.com/item?id=50383112
그리고 단어를 엉망으로 쓴 예가 하나 더 있습니다. “대수와 기하 사이에 ‘광범위한 사전(sweeping dictionary)’을 만들어, 수학자들이 임의의 환 위에서 기하를 할 수 있게 했고, 산술 및 무한소 데이터가 처음부터 내장되어 있다.”
“sweeping dictionary”가 대체 무슨 뜻입니까?! 그리고 “creating ... across” 같은 식으로 간접 목적어를 이끄는 것도 맞는 방식이 아니라고 생각합니다. 예전 글쓰기 수업에서는 “어색한 구문”이라고 불렀겠지만, 다들 AI가 만드는 이런 어색한 구문에 너무 익숙해져 있습니다.
“대수와 기하 사이에 연결 고리를 만들어, 수학자들이 임의의 환 위에서 기하를 할 수 있게 했고, 산술 및 무한소 데이터가 처음부터 내장되어 있다.”라고 쓸 수도 있었을 겁니다. 사실 제가 익숙한 표현은 이쪽입니다.
안타까운 일입니다. 은유를 즉흥적으로 비트는 건 멋질 수 있지만, LLM은 그걸 끊임없이, 그것도 형편없이 합니다. 그러면 엄마가 (시뮬레이션된) 아이들을 바라보며 “이러니까 좋은 걸 못 갖는 거야”라고 말하는 꼴이 됩니다.
수정: 참을 수가 없네요. “…정의와 정리로 이루어진, 촘촘하게 상호 연결된(interconnected) 의존성 그래프에서…”
물론 connected와 interconnected는 거의 같은 뜻입니다. 하지만 수학에서 그래프는 connected라고 말하지 interconnected라고 하지 않습니다. 미묘한 어법이지만, 나쁜 미묘함도 쌓이면 무시 못 합니다. 정말이지.
“…처음부터 내장되어 있다(built in from the start)”도 상투적인 표현이고, 사전 비유와도 안 맞아요.
이거 보고 웃음이 터졌어요. 그로텐디크식 기하학이 LLM 말투로 묘사되는 걸 보게 될 줄은 몰랐거든요. 참 대단한 시대예요.
그 말이 상투적인 AI 카피보다 훨씬 더 짜증 나요.
맞아요, “이 이정표는 Stacks Project 자체에서 시작됩니다(This milestone begins with the Stacks Project itself)”라는 문장 말이죠. “은유를 섞거나 뒤틀지 마”라는 프롬프트만 줘도 AI 슬롭 효과의 절반은 줄일 수 있지 않을까요? 마일스톤은 과정 안의 한 단계이지, 과정 전체가 아니잖아요.
예전에는 이렇게 인상적으로 들리려는 엉성한 노력은 그냥 “과장된 글”이었는데, 이제는 AI라는 강력한 신호가 됐어요.
그게 왜 혼합 은유인가요? 저는 큰 마일스톤이 여러 개 있고 각 마일스톤마다 여러 프로젝트가 얽힌 대규모 이니셔티브나 프로그램에 아주 익숙한데요. 문제될 게 전혀 안 보여요.
그들이 도달하는 마일스톤은 Stacks Project의 형식화입니다. 그건 AI에 그걸 시키기 시작했을 때, 혹은 미리 계획을 짰을 때부터 시작된 거고요.
마일스톤이라는 은유는 더 큰 과정 안에서 달성한 목표를 가리킵니다. 이런 (제 생각엔 잘못된) 쓰임의 개별 사례에서 문제를 못 느끼는 사람이 많은 건 맞지만, AI는 그런 걸 줄줄이 만들어 내고, 그게 쌓여 AI 글 특유의 분위기가 생깁니다. 어느 부분이 문제인지 콕 집어 말하진 못해도 많은 사람이 그 분위기를 느끼죠.
주제에서 살짝 벗어나지만, (이를테면) WebDAV나 NFS 서버를 위한 형식 검증된 스택은 얼마나 멀리 있을까요?
Stacks Project가 다루는 건 대수적(그리고 기하적) 스택이에요. 하강(descent)을 통해 일반화한 스킴인데, 층(sheaf)이나 군포이드 올(groupoid fibre) 같은 걸 써서요.