Axiom이 AI 에이전트로 유한 단순군 분류 증명을 Lean으로 검증했다고 발표했어요. 원본 약 1만 5천 쪽 증명이 24일, 4,310만 줄 코드로 옮겨졌다고 해요. 다만 수치는 전부 회사 발표라 독립 검증이 관건이에요.
수학 좀 아는 분들한테 "유한 단순군 분류"는 좀 전설 같은 이름이에요. 수십 년에 걸쳐 수백 명이 쓴 500편이 넘는 논문을 합치면 원본 증명이 대략 1만 5천 쪽이라서, 흔히 "거대 정리(Enormous Theorem)"라고 부르거든요. 그런데 10월 26~27일 사이에 AI 스타트업 Axiom Math가 이걸 컴퓨터로 끝까지 검증했다고 발표했어요. 🔬
방식이 좀 인상적이에요. 수학자와 엔지니어가 방향을 잡고, 수십 개 에이전트가 무리를 지어 일했다고 해요. 전체를 108개 마일스톤, 약 380개의 작은 작업으로 쪼갠 다음 에이전트들이 GitHub 이슈로 일을 가져가고, 리드 에이전트가 정리(statement)가 맞는지 검토하는 사이에 다른 에이전트들이 증명을 썼대요. 사람 조직이 일하는 방식이랑 거의 똑같죠.
결과물은 Lean 코드 약 4,310만 줄이고, 걸린 시간은 24일이에요. 📊 참고로 올해 8월에 올라온 별도 학술 연구(FormaTheoria)는 같은 분류의 주요 부분을 약 99만 줄 Lean으로 옮겼다고 했는데, 그 규모와 비교하면 이번 발표가 얼마나 큰 점프인지 감이 와요. 한 매체는 Axiom의 에이전트가 원래 논증 중 한 닫힘(closure) 주장에 대한 반례도 찾아냈다고 전하고 있어요.
근데 여기서 한 번 숨을 고르고 싶어요. 지금 나온 숫자는 전부 Axiom이 직접 센 거예요. 저장소와 전문가 검토를 통한 독립 확인은 아직 못 봤어요. 그리고 Lean이 "맞다"고 해주는 건 형식화된 명제가 증명과 맞는다는 뜻이지, 그 명제가 원래 수학자들이 의도한 정리와 정확히 같다는 보장까지는 아니에요. 이 부분은 사람이 읽고 확인해야 하는 영역이에요. ⚠️
솔직히 저는 증명이 맞느냐보다 "증명 검증이 이제 노동의 문제가 됐다"는 쪽이 더 놀라워요. 예전엔 이런 형식화가 수년짜리 프로젝트였는데, 이제는 컴퓨트와 오케스트레이션 문제로 바뀌고 있다는 신호잖아요. 며칠 전 OpenAI가 새 수학 결과를 주장했을 때도 "누가 확인하나"가 쟁점이었는데, 이번엔 확인하는 쪽 자체를 AI가 맡는 그림이에요.
그럼 앞으로 논문에 Lean 증명이 붙는 게 기본값이 될까요? 아니면 4천만 줄짜리 코드를 읽을 사람이 없다는 새 문제가 생길까요? 저도 아직 잘 모르겠어요.
출처