요약
AI 에이전트를 동원해 유한 단순군 분류 정리의 1세대 증명 전체를 Lean으로 옮겼습니다.
액시엄 매스 연구진이 공개한 프로젝트입니다. 이 정리는 모든 유한 단순군(더 작은 군으로 쪼갤 수 없는 유한군)이 몇 가지 부류로 나뉜다는 내용입니다. 약 100명의 수학자가 수십 년 동안 수천 쪽의 논문으로 증명했습니다.
왜 중요한가
- 사람이 끝까지 검토하기 어려웠던 거대한 증명을 Lean 커널(증명의 각 단계를 확인하는 검사기)이 한 단계씩 확인했습니다.
- 형식화 과정에서 출판된 증명의 오류가 실제로 드러났습니다.
- 수백 편의 문헌에 흩어진 증명도 AI 에이전트로 형식화할 수 있다는 사례입니다.
핵심 내용
- 모든 유한 단순군은 소수 차수 순환군, 교대군, 리 형 군, 26개 산재군 가운데 하나라는 결론까지 검증했습니다.
- 결과물은 Lean 코드 4,310만 줄, 선언(정의와 정리) 205만 개 규모입니다.
- 논문과 책 715편을 근거로 삼았고, 에이전트에게 처음 준 설계도를 따라 100개 단계로 나눠 진행했습니다.
- 불균형군 정리(Unbalanced Group Theorem)의 출판된 증명에 쓰인 한 주장에서 반례를 찾았습니다.
- 연구진은 솔로몬의 1976년 이론에 기댄 우회 증명을 35쪽 논문으로 냈고, 군론 학자들과 문헌의 정오표도 정리하고 있습니다.
HN 반응
- 원래 증명이 1만 쪽에 이르고 과거에도 빈틈이 드러났던 만큼 기계 검증의 가치가 크다는 반응이 많았습니다.
- 액시엄 측은 에이전트 무리가 500편 넘는 문헌을 맡았다고 밝혔고, 문헌마다 다른 정의를 하나로 맞추는 일이 난제로 꼽혔습니다.
궁금해서 여쭙는데, 최첨단 모델 하나를 세상에 있는 모든 수학 교과서에 풀어놓고 증명, 정리, 보조정리 같은 걸 하나도 빠짐없이 Lean으로 바꾸게 하는 건 불가능한가요? 최첨단 모델이라면 할 수 있을 것 같은데요. 게다가 한 번만 하면 되는 일이잖아요. 한 번 해 두면 영원히 남아서 다른 증명에서 라이브러리로 가져다 쓸 수 있고요.
제가 Lean을 잘못 이해하고 있는 걸 수도 있어요. 저는 수학을 위한 프로그래밍 언어쯤으로 생각하고 있거든요.
저는 Axiom의 MTS입니다. 말씀하신 방식이 이번 증명을 형식화한 방법과 꽤 비슷합니다. 이 증명은 500편이 넘는 논문과 책에 흩어져 있었고, 에이전트 떼를 투입해 그 자료들을 모두 훑게 했습니다.
어려운 점 하나는 이 모든 걸 일관된 하나로 조립하는 일입니다. 같은 비형식적 개념도 서로 조금씩 다르고 호환되지 않는 방식으로 형식화될 수 있기 때문입니다.
그 에이전트들은 무엇을 기반으로 했나요?
저는 수학 배경이 들쭉날쭉하고 기초적인 수준이라서 하는 말인데요, 증명을 단순화하고 여러 조각을 일관된 하나로 묶는 건 컴퓨터가 제일 잘하는 일일 줄 알았거든요. 그런데 제가 보고 들은 바로는 전혀 그렇지 않은 것 같아요. 왜 그런지 설명해 주실 수 있나요?
컴퓨터가 실제로 잘하는 (보통은 작은) 단순화가 있습니다. 컴파일러 최적화와 비슷하다고 보시면 됩니다. 증명이 사실상 보조정리 몇 개를 이어 붙인 것이고 중간 작업 일부를 덜어낼 수 있다는 걸 알아보고 그렇게 바로 이어 주는 식입니다. Lean에서는 짧거나 중간 길이인 증명을 LLM에 넣으면 이런 사소한 개선안을 제시해 주는 경우가 많습니다.
반면 정말 큰 차이를 만드는 개선, 즉 대폭적인 단순화 같은 건 그다지 잘하지 못합니다. 이게 어떻게 돌아가는지 알면 그리 놀라운 일은 아닙니다.
먼저 Lean의 증명은 (다른 증명 보조기 대부분도 마찬가지일 겁니다) 본질적으로 가설을 받아서 특정 타입의 값을 만들어 내는 함수입니다. 그 타입은 (커리-하워드 대응 덕분에) 어떤 명제의 증명과 같습니다. 증명 보조기는 의존 타입 이론을 이용해 매 단계에서 타입이 모두 맞아떨어지는지 확인하고, 이것이 엄밀성을 보장합니다. 그러니 증명을 단순화하는 일은 사실상 무한 차원의 공간에서 경로를 찾는 일입니다. 출발점과 도착점은 알지만, 한 걸음 한 걸음은 정당화만 할 수 있다면 사실상 어느 방향으로든 갈 수 있습니다. 걸음의 정당화는 표준 라이브러리에 있는 (지금은 방대한) 보조정리와 정리 중에서 골라 쓰거나, 단순화하려고 쓰는 바로 그 과정을 재귀적으로 적용해 그 걸음에 필요한 증명이나 함수를 직접 만들어서 합니다. 대단히 유연하지만, 선택지가 너무 많아서 오히려 계획을 세우기가 어렵습니다.
둘째로, "종이와 펜"으로 쓰는 증명에서 LLM은 인간 수학자에게 어떤 단계가 중요하고, 쉽고, 어렵고, 직관적이거나 직관에 반하는지를 구분하지 못합니다. 그래서 LLM이 내놓는 증명은 많은 부분이 극도로 투박하고 지나치게 꼼꼼합니다. 누가 봐도 뻔해서 보통은 건너뛸 세부 사항에 오래 머무르다가, 더 공을 들여야 할 부분은 아주 빠르게 지나가 버립니다. 이런 들쭉날쭉함 탓에 사람이 따라가기 어려운 증명이 나오기도 하지만, 무엇이 쓸 만한 단순화인지 판단하는 능력도 대체로 떨어진다는 뜻입니다.
증명과 프로그램은 쌍둥이입니다. 형식화된 정리들이 서로 호환되지 않는 이유는 프로그래밍 API들이 호환되지 않는 이유와 똑같을 수 있습니다.
어쩌면 증명용 OpenAPI나 gRPC 같은 게 나와서 이 문제를 어느 정도 풀어 줄 수도 있겠네요. 아니면 lean4가 이미 그 역할을 하고 있는 걸 수도 있고요.
서로 관련 없는 예를 몇 가지 들어 보겠습니다.
어떤 책은 0을 자연수로 보고, 다른 책은 1부터 시작합니다.
어떤 책에서는 모든 환(https://en.wikipedia.org/wiki/Ring_(mathematics))이 곱셈 항등원을 갖습니다. 대수(Algebra)도 거의 모든 책이 항등원이 있다고 가정하지만, 이상한 예외가 있을 수 있습니다.
어떤 책은 첫 페이지에서 앞으로 모든 군이 아벨 군(가환군)이라고 가정하겠다고 밝히고, 이후 페이지마다 그 가정을 되풀이하지 않습니다.
푸리에 변환을 정의하는 관례만 8가지쯤 됩니다. 모두 동등하지만 저마다 여기저기에 서로 다른 상수가 붙습니다. 다른 책의 공식을 섞어 쓸 때는 조심해야 합니다.
각 책과 논문에 나오는 이름을 하나로 일관된 정의 체계에 맞춰 옮기며 세부 사항을 추적하고 기억하는 일은 컴퓨터가 더 쉽게 할 것 같습니다.
두 출처가 같은 대상을 서로 호환되지 않는 방식으로 형식화했을 때, 에이전트 떼는 대체로 둘 사이를 잇는 번역 보조정리를 만들어 냈나요, 아니면 누군가 정본이 될 정의를 하나 고르고 그 뒤에 오는 증명들을 거기에 맞게 다시 쓰게 했나요? "일관된 하나"를 만드는 비용은 실제로는 두 번째 쪽에 있을 것 같은데요. 출처 500개를 다룬 작업에서 이런 조정 작업과 한 줄씩 옮기는 번역 작업이 각각 얼마나 차지했는지 궁금합니다.
맞아요, 다만 기초적인 내용조차 서술 방식이 무수히 많아서, 그중 어느 것을 라이브러리에 넣을지는 사람이 정해야 합니다. 물론 교과서가 가끔 그러듯 동등한 서술을 두세 개, 대여섯 개, 열 개씩 넣을 수는 있지만, 그래도 세상의 모든 걸 다 넣을 수는 없죠.
아마 앞으로 몇 달 안에 어떤 형태로든 이뤄질 겁니다.
제가 보기에 이 문제에서 정말 흥미로운 부분은 어떤 정리 서술들이 전체로서 잘 맞물리는지를 알아내는 일입니다. 소프트웨어 아키텍처 문제와 아주 비슷합니다.
Metamath가 이 분야에서 상당한 기초 연구를 했습니다. 정리는 표준적이지는 않아도 더 일반적인 형태로 서술되는 경우가 많습니다.
이런 질문도 던져 볼 수 있습니다. "함수형 프로그래밍에 해당하는 건 무엇일까?" 혹은 "전역 상태가 있을까?" 같은 것들요. 역수학(reverse mathematics)에 대한 하나의 관점입니다.
참고로 mathlib에는 지금도 중복된 정리가 많이 들어 있습니다. 중복 제거가 적극적인 목표로 잡혀 있는 걸로 알고 있어요. 지금 한창 공을 들이고 있는지는 모르겠지만요.
이래저래 그렇기도 하고 아니기도 합니다. 컴퓨팅 자원이 충분하면 아마 가능하겠지만, 그렇게 한다고 해서 꼭 재사용할 수 있는 라이브러리가 나오는 건 아닙니다. https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/ 를 보세요.
정말 대단한 일이고, 저에게는 아주 중요한 소식입니다. 저는 이 분류에 대해 늘 의구심을 품어 왔는데, 이렇게 방대한 증명이 옳다고 검증된 걸 보니 지금까지 우리가 수학을 해 온 방식에 큰 확신이 생깁니다.
이건 자동 형식화를 아주 잘 활용한 사례 같아요. 과거에 수학자들이 분류를 끝냈다고 잘못 믿었다가 빠진 군이나 산재군(sporadic group)을 뒤늦게 발견한 적이 있으니까요.
원래 증명은 수학자 약 100명이 협업한 결과인데, 테렌스 타오의 말이 맞다면 앞으로 물리학처럼 이런 협업을 더 많이 보게 될 거예요.
빠진 산재군을 발견한 적은 없습니다. 증명의 큰 틈(quasithin 경우)은 600쪽짜리 미출간 원고가 그 부분을 다루고 있었는데, 나중에 조사해 보니 그 원고가 불완전했기 때문에 생긴 겁니다.
그리고 흥미로운 건 형식화가 빠진 경우를 잡아내는 데서 그치지 않고, 모두가 당연하게 여겨 온 모든 가정을 하나하나 따져 보게 만든다는 점이에요.
저는 군(group)이 추상대수학으로 들어가는 입문 약물이었어요. 친구가 대칭이 어디에나 있고 군이 바로 대칭을 형식화한 것이라고 알려 줬는데, 그걸 이해해 가는 과정이 정말 어마어마한 여정이었죠. 최첨단 모델들은 그런 추상 개념을 쉬운 영어 예시와 연결해 주고 질문에도 꽤 잘 답해 줘요. 혼자서 이 분야를 시작해 무엇을 보여 주는지 확인해 보기에 지금처럼 좋은 때는 없었어요.
호모토피 기반 쪽 사람들이 끝내 정신을 못 차려서, 형식화가 이렇게 성숙해진 지금도 여전히 집합론 기반으로 하고 있다는 게 참 슬퍼요.
저희는 꾸준히 앞으로 나아가고 있어요 :) https://github.com/marcinjangrzybowski/cubical-bis/blob/integrate-lorenzo-premetric-fast-rationals/Cubical/AnalysisC/SCOPE_ROADMAP.md (문서 중간의 표를 보세요.) 완전히 구성적인 구현이라서 모든 실수 표현식에 대해 임의 정밀도의 근삿값을 얻을 수 있다는 점을 염두에 두세요. 아직은 작업 중이지만 곧 cubical-library에서 쓸 수 있게 될 거예요 :) 관련해서 TYPES2026에서 한 발표도 있어요: https://types2026.cse.chalmers.se/slides/51.pdf
지난주에 Claude Max 주간 사용량을 전부 써 가며 Opus에게 Mathlib을 Coq-HoTT로 옮기게 했어요. 너무 아름다워서 이번 주에 또 하고 싶어 못 견디겠네요.
아니요, 타입 이론이 이겼습니다. 페르 마르틴뢰프는 아직 살아 있으니, 자신의 연구가 어떤 형태로든 Lean에 살아 있다는 걸 확인해 줄 수 있을 겁니다. 반면 체르멜로와 프렝켈은 완전히 어리둥절해하겠죠.
하시려던 말은 Lean이 HoTT가 아니고, Mathlib에는 고전 논리(배중률, 선택 공리)를 쓴 추론이 아주 많다는 거겠죠.
HoTT에게 너무 늦었다고는 전혀 생각하지 않습니다. 오히려 AI 기업들이 분포를 벗어난 이상한 방식으로 새 수학을 더 많이 찍어 내 보는 게 아주 유용한 연습이라는 걸 알게 될 거라고 봅니다.
그분이 그렇게 말씀하실지는 잘 모르겠네요. 페르 마르틴뢰프의 원래 작업은 비숍(Bishop) 식 구성적 수학을 위한 계산적이고 서술적(predicative)인 기초를 세우는 것이었습니다.
Lean의 타입 이론은 그 발상을 사실상 포기했습니다. Mathlib은 선택 공리와 몫 타입 등과 함께 비서술적(impredicative) 명제를 신나게 가정합니다. 종합하면 Lean은 정신 면에서 드 브라위너의 AUTOMATH 프로젝트(마르틴뢰프보다 앞선 것입니다!)에 훨씬 가깝다고 봅니다. 이 프로젝트의 목표는 의존 타입을 써서 고전 수학 교과서를 형식화하는 것이었습니다.
제 말은 마르틴뢰프가 mathlib이 아니라 Lean에서 자신의 작업을 알아볼 거라는 겁니다. Mathlib은 라이브러리일 뿐이에요. Lean에서는 고전 논리를 코드베이스의 특정 부분에 "가둬 둘" 수 있고, 이건 원래의 MLTT에서도 마찬가지입니다. 고전 공리를 범위 안의 함수로 가정하면 되니까요.
틈이 하나만 발견됐다니 놀랍네요. 특히 결과가 여러 사람이 쓴 많은 논문에 걸쳐 흩어져 있었으니, (고칠 수 있는) 틈이 여러 개 드러날 줄 알았거든요.
[1]에서는 이렇게 주장합니다.
[1] https://axiommath.ai/research/the-enormous-theorem-formalized/
지난 40년 동안 이미 (사람들이) 수많은 틈을 찾아내 메웠습니다.
형식화 분량은 Lean 코드 4,310만 줄입니다.
그게 수학적으로 쓸모가 있을까요?
아무것도 놓치지 않았다는 걸 알 수 있다는 점은 좋죠. 자연어 증명은 1만 쪽에 달하고, 과거에 군을 빠뜨린 적도 있으니까요.