Classification of Finite Simple Groups Formalized in Lean
Lean으로 형식화한 유한 단순군 분류
Axiom Math가 유한 단순군 분류의 1세대 증명을 Lean으로 완전히 형식화했다고 발표했습니다. 형식화 과정에서 불균형 군 정리의 기존 증명에 문제가 있음을 발견해 대안 증명을 제시했고, Lean 커널이 각 논리 단계를 검사합니다.
- 주제
에디터 노트
Lean 형식화의 가장 구체적인 성과는 분류 정리를 다시 적은 데 그치지 않고, 불균형 군 정리의 출판된 논증에서 성립하지 않는 주장을 찾아 대안 증명을 마련했다는 점입니다. 연구팀은 Lean 커널이 형식화된 증명을 검사한다고 설명하지만, 이 검사는 형식화한 명제와 정의가 의도한 수학적 내용과 일치하는지까지 자동으로 보증하지는 않습니다. 댓글에서도 커널 버그와 잘못 형식화한 명제가 서로 다른 위험으로 제기됩니다. 댓글은 형식 검증이 긴 증명의 누락을 확인하는 데 유용하다고 보는 한편, 과거에 발견된 여러 공백은 이미 사람이 고쳤다는 점과 이번 작업에서 문헌과 대조해 해결한 차이가 34건이었다는 주장을 덧붙입니다. 따라서 이번 결과는 과거의 오류를 모두 AI가 찾아냈다는 사례라기보다, 대규모 증명을 기계가 검사할 수 있는 형태로 통합하면서 문헌의 논증을 재검토한 사례로 보는 편이 정확합니다. 형식화가 재사용 가능한 수학 라이브러리로 이어지는지는 별도의 설계 과제로 남습니다.
AI 요약
유한 단순군 분류는 모든 유한 단순군이 소수 차수 순환군, 교대군, 리형 군 또는 26개의 산발 단순군 가운데 하나라고 밝힌 정리입니다. 원래 증명은 수십 년에 걸쳐 약 100명의 수학자가 쌓은 수천 쪽 분량의 논문으로 이뤄졌습니다. Axiom Math는 이 1세대 증명을 Lean으로 완전히 형식화했다고 발표했습니다. 증명의 각 논리 단계는 Lean 커널이 검사합니다.
형식화 과정에서 발견한 증명 문제
연구팀은 1세대 증명을 Lean에 옮기는 과정에서 불균형 군 정리(The Unbalanced Group Theorem)에 쓰인 출판된 증명 경로의 폐포 관련 주장이 성립하지 않는 반례를 발견했습니다. 새 논문은 그 장애물을 설명하고, 단순군의 경우 Solomon이 1976년에 발전시킨 최대 2-성분(maximal 2-components) 이론을 이용한 대안 논증을 제시합니다. 이 논증의 주요 단계는 단순한 꼭대기(simple tops)의 보존을 보이는 정리 2.3입니다. 연구팀은 문헌에서 발견한 정정 사항을 군론 연구자들과 정리해 공개할 계획이라고 밝혔습니다.
형식화의 규모와 범위
프로젝트는 500편이 넘는 논문과 책에 흩어진 증명을 하나의 Lean 형식화로 엮었습니다. Hacker News 댓글에서 참여자는 Lean 코드가 4,310만 줄이라고 전했습니다. 다만 이 수치는 댓글에 제시된 값이며, 제공된 프로젝트 본문에는 코드 규모가 나오지 않습니다. 프로젝트 소개는 1세대 증명을 따랐다고 설명하며, 정리 자체의 명제뿐 아니라 이를 뒷받침하는 논리적 단계들을 커널 검사 아래 두었다고 밝힙니다.
Hacker News 반응
- @pfdietz — Lean 코드가 4,310만 줄입니다.
- @bwestergard — 수학적으로 쓸모가 있을까요?
- @sebzim4500 — 과거에도 수학자들이 분류를 끝냈다고 믿었다가 빠진 경우나 산발 단순군을 나중에 발견한 적이 있으니, 빠뜨린 것이 없다는 점을 확인하는 데 의미가 있습니다. 자연어 증명은 1만 쪽이며 과거에도 군을 놓친 적이 있습니다.
- @Panoramix — 형식화 자체에 오류가 없다는 점은 어떻게 확인하나요? 형식화가 사소한 작업은 아닌 것으로 압니다.
- @sebzim4500 — 정의가 올바른지 확인하는 일은 대체로 어렵지 않습니다. 검증에 쓰는 Lean 커널 가운데 하나가 올바르다고 가정하면 됩니다. 물론 구현들이 서로 기반을 공유하므로 공통 버그가 있을 가능성은 가정에 남습니다. 이번 명제는 유난히 복잡하지만 증명 전체보다 검증하기는 훨씬 쉽습니다.
- @kenferry — 컴퓨터로 형식화하는 목적은 검증 가능성입니다. 형식화 오류라면 Lean 버그일 수 있습니다. 거대한 증명이 Lean 버그를 찾는 LLM을 부추길 수 있다는 생각도 해봤지만, 검증 대상이 더 작다는 이점은 있습니다.
- @adrianN — 형식화 오류는 증명했다고 생각한 것과 다른 명제를 실제로 증명하는 경우일 수도 있습니다.
- @cvoss — 이번 형식화 작업은 원래 출판물의 잘못된 논증을 찾아내고 우회해 결과를 보완했습니다.
- @curt15 — Lean이 논리 오류를 찾아낸다는 점에서 더 의미가 있습니다. 2세대 증명도 진행 중입니다.
- @pfdietz — 증명이 워낙 복잡하고 길어 의문이 남아 있었는데, 이번 작업으로 그런 의문이 해소됩니다.
- @cubefox — 아마 Lean 증명 가운데 압도적으로 가장 긴 것 같습니다.
- @pfdietz — 공백과 주석을 리눅스 코드에서 세는지에 따라 다르겠지만, 어떤 종류든 가장 긴 오픈소스 프로젝트일 수도 있습니다.
- @cubefox — 2100년까지 AI 없이 사람이 완성할 수 있었을까요?
- @cvoss — 어렵다고 봅니다. 원래 증명이 여러 곳에 흩어졌고 오래된 부분도 있으며, 처음 시도한 증명이라 간결하거나 명료하지 않은 대목도 있습니다. 결과가 왜 성립하는지 아는 사람들의 경험이 사라질 위험이 있었습니다. 2세대 증명은 수만 쪽에서 약 5,000쪽으로 정리하는 작업이며, 2세대가 끝나기도 전에 이를 다시 압축하는 3세대 프로젝트도 시작됐습니다. 두 작업 모두 아직 진행 중인 것으로 압니다.
- @sebzim4500 — Lean의 수십 년간 발전을 포함하는지에 따라 다릅니다. 비AI 자동 증명도 최근까지 빠르게 나아졌고, 사람들도 이런 프로젝트의 정의와 모듈 구조를 정하는 법을 배울 것입니다.
- @sebzim4500 — 과거 수학자들이 분류를 마쳤다고 생각했다가 뒤늦게 빠진 부분을 발견한 사례를 고려하면, 자동 형식화의 좋은 활용으로 보입니다. 원래 증명도 약 100명의 협업이었으니 물리학처럼 이런 협업이 더 늘 수 있습니다.
- @QuesnayJr — 빠진 산발 단순군을 발견한 것은 아닙니다. 증명의 큰 공백인 준박형(quasithin) 경우는 600쪽짜리 미출판 원고가 다룬다고 여겼지만, 나중에 검토하니 미완성이었습니다.
- @jonath_laurent — Axiom Math 소속입니다. 말씀하신 방식은 이번 형식화와 상당히 비슷합니다. 500편이 넘는 자료를 여러 에이전트가 조사했습니다. 비형식 수학의 같은 개념을 서로 조금 다르면서 호환되지 않는 방식으로 형식화한 자료를 일관된 체계로 모으는 일이 과제였습니다.
- @whatshisface — 에이전트는 어떤 모델을 기반으로 했나요?
- @bananaflag — 기초 정리도 여러 방식으로 표현되므로 어떤 표현을 라이브러리에 넣을지 사람이 결정해야 합니다. 동치인 표현을 몇 가지 넣을 수는 있어도 모든 표현을 담을 수는 없습니다.
- @QuesnayJr — 여러 논문과 여러 사람에게 흩어진 증명이라면 고칠 수 있는 공백을 더 많이 발견할 줄 알았습니다.
- @contubernio — 지난 40년 동안 사람이 이미 많은 공백을 찾아 고쳤습니다.
- @bamb008 — Axiom Math의 연구 글은 출판 기록과 달라 해결해야 했던 눈에 띄는 차이가 34건이었고, 가장 큰 문제는 불균형 군 정리였다고 인용합니다.
원문: Axiom Math / 번역·요약: Trawling