만 쪽이 넘는 증명이 컴퓨터 안으로
수학에는 ‘증명은 끝났는데 처음부터 끝까지 다 읽어본 사람은 거의 없는’ 정리가 있어요. 바로 유한 단순군 분류 정리(CFSG, Classification of Finite Simple Groups)예요. 100명이 넘는 수학자가 수십 년 동안 수백 편의 논문으로 쌓아 올린 증명인데, 분량이 흔히 1만 쪽이 넘는다고 해요. 1980년대 초에 완성이 선언됐다가 빈틈이 발견되는 바람에, 2004년에야 quasithin case라고 불리는 마지막 조각이 메워졌을 정도예요.
이번에 AI 수학 스타트업 Axiom이 이 정리를 정리 증명기 Lean으로 형식화했다는 발표 페이지를 공개했어요. 사람이 쓴 거대한 증명을 컴퓨터가 한 줄씩 검증할 수 있는 형태로 옮겼다는 뜻이라, 수학계는 물론 개발자에게도 의미가 큰 소식이에요.
유한 단순군이 뭐냐면
먼저 군(group)은 ‘이어 붙일 수 있고 되돌릴 수도 있는 동작들의 모임’이에요. 루빅스 큐브 돌리는 동작을 떠올리면 쉬워요. 두 동작을 이어서 하면 또 하나의 동작이 되고, 모든 동작에는 그걸 되돌리는 동작이 있죠.
단순군은 더 작은 군으로 쪼갤 수 없는 군이에요. 자연수에서 소수가 그런 것처럼요. 실제로 조르당-횔더 정리에 따르면 모든 유한군은 단순군들로 분해되고, 그 구성 요소는 하나로 정해져요. 소인수분해랑 똑같죠. 그러니 유한 단순군을 전부 찾아내는 일은 화학에서 원소 주기율표를 완성하는 일과 같아요.
결론은 이래요. 모든 유한 단순군은 소수 크기의 순환군, 교대군, 리 형(Lie type) 군으로 이루어진 18개의 무한 가족 중 하나에 속하거나, 어느 가족에도 들지 않는 26개의 산재군(sporadic group) 중 하나예요. 산재군 가운데 가장 큰 ‘몬스터 군’은 원소가 약 8×10^53개나 돼요.
형식화가 뭐냐면
형식화(formalization)는 증명을 컴퓨터가 검사할 수 있는 언어로 다시 쓰는 작업이에요. 개발자에게 익숙한 비유를 들면, 수학 논문은 동료가 눈으로 리뷰하는 코드이고 형식화된 증명은 컴파일러의 타입 체커를 통과한 코드예요. 사람의 리뷰는 아무리 꼼꼼해도 놓치는 게 있지만, 타입 체커는 한 줄의 비약도 그냥 넘기지 않거든요.
Lean은 마이크로소프트 리서치에서 시작된 언어예요. 지금의 Lean 4는 정리 증명기이면서 일반 프로그래밍 언어이기도 해요. ‘명제는 타입이고 증명은 그 타입의 값’이라는 커리-하워드 대응 덕분에 증명을 쓰는 일이 곧 프로그램을 짜는 일이 돼요. 예를 들어 [Group G] [Fintype G] [IsSimpleGroup G] 같은 조건을 붙인 정리 선언은 ‘G가 유한 단순군이라면 무엇이 성립한다’는 명제를 타입으로 표현한 거예요. 여기에 수학 정리를 모아둔 거대한 커뮤니티 라이브러리 Mathlib까지 있어서, 기초 정리를 매번 처음부터 증명할 필요도 없어요.
왜 이게 대단할까
규모를 비교해 보면 감이 와요. CFSG의 한 조각에 불과한 파이트-톰프슨 정리(홀수 크기의 유한군은 가해군이다)를 Coq로 형식화하는 데 조르주 공티에 팀이 약 6년을 썼고, 2012년에야 끝냈어요. 그런 조각이 수없이 모인 게 CFSG니까, 기존 방식이었다면 수십 년짜리 프로젝트였을 거예요.
그래서 Axiom이 AI 기반 증명 시스템을 만드는 회사라는 점이 관전 포인트예요. 2024년 딥마인드의 AlphaProof가 국제수학올림피아드에서 은메달 수준 성적을 낸 뒤로, AI가 Lean 증명을 만들어내는 기술은 빠르게 발전해 왔거든요. AI가 증명을 쓰고 Lean 커널이 검증하는 구조라면 AI의 ‘환각’을 걱정할 필요가 없어요. 틀린 증명은 애초에 통과하지 못하니까요.
꼭 확인해야 할 포인트
다만 형식화 소식을 볼 때는 몇 가지를 직접 확인하는 습관이 필요해요.
sorry가 남아 있는지: Lean에서sorry는 ‘여기는 일단 증명된 걸로 치자’는 임시방편이에요. 코드의 TODO 주석 같은 거죠.- 추가 공리를 선언했는지:
#print axioms 정리이름을 실행하면 그 정리가 어떤 공리에 기대고 있는지 볼 수 있어요. - 정리의 진술이 원래 수학과 같은지: 증명이 맞아도 ‘무엇을 증명했는지’를 잘못 옮겼다면 의미가 없어요. 소프트웨어로 치면 테스트는 통과했는데 스펙이 틀린 경우예요.
한국 개발자에게 주는 시사점
형식 검증은 이미 소프트웨어 업계에서도 쓰이고 있어요. seL4 마이크로커널과 CompCert C 컴파일러가 대표적이고, AWS는 접근 제어 정책 언어 Cedar를 Lean으로 검증하고 있어요. AI가 코드를 점점 더 많이 쓰는 지금, ‘AI가 짜고 기계가 증명하는’ 방식은 앞으로 더 중요해질 거예요.
입문하고 싶다면 브라우저에서 바로 해볼 수 있는 Natural Number Game과 공식 문서 Functional Programming in Lean을 추천해요. 함수형 프로그래밍에 관심 있는 분이라면 생각보다 빨리 손에 익을 거예요.
마무리
한 줄 정리: 인류가 쓴 가장 거대한 증명이 기계 검증의 영역으로 들어왔고, 이건 수학뿐 아니라 ‘검증 가능한 AI’의 미래를 보여주는 신호예요.
AI가 만든 코드도 언젠가 이렇게 수학적으로 검증받아야 하는 날이 올 거라고 보시나요? 형식 검증을 실무에서 써본 경험이 있다면 함께 나눠주세요!
🔗 출처: Hacker News