문제부터 볼게요: 정사각형 11개를 가장 작은 상자에
한 변이 1인 정사각형 타일 n개를 겹치지 않게 넣으려면, 정사각형 상자의 한 변이 최소 얼마여야 할까요? 4개면 2, 9개면 3이에요. 여기까진 너무 쉽죠. 재밌어지는 건 제곱수가 아닐 때예요. 5개라면 네 모서리에 하나씩 놓고 가운데에 하나를 45도 기울여 끼우는 게 최선이에요. 이때 상자 한 변은 2+1/√2, 약 2.707이에요.
개수가 늘수록 문제는 급격히 어려워져요. 10개는 3+1/√2(약 3.707)가 최적이라는 사실이 2003년에야 Walter Stromquist에 의해 증명됐어요. 그리고 11개가 있어요. 1979년 Walter Trump가 한 변 약 3.877짜리 배치를 찾았는데, 그림을 보면 정사각형 몇 개가 묘한 각도로 비스듬히 끼어 있어서 '이게 정말 최선이라고?' 싶은 모양이에요. 그 뒤로 40년 넘게 아무도 더 좋은 배치를 찾지 못했지만, 이게 최적이라는 증명도 없었어요.
이번에 공개된 GitHub 저장소는 이 배치가 최적이라는 걸 AI의 도움을 받아 증명하고, 그 증명을 형식화(formalize)했다고 밝혀요. 수학계의 검증은 아직 진행 중이라고 보는 게 맞지만, 접근 방식만으로도 살펴볼 가치가 충분해요.
'최적임을 증명한다'는 게 왜 이렇게 어려울까
더 좋은 배치를 찾는 쪽은 비교적 쉬워요. 예시 하나만 보여주면 끝이거든요. 반면 최적이라는 걸 증명하려면 이보다 작은 상자에는 어떤 방법으로도 안 들어간다는 걸 보여야 해요. 정사각형마다 위치(x, y)와 회전 각도가 있으니 11개면 변수가 33개이고, 하나하나가 연속적인 실수라서 경우의 수가 무한해요.
그래서 보통은 가능한 배치 공간을 잘게 나눠서 '이 영역에서는 안 된다'를 하나씩 보여요. 여기에 컴퓨터 계산을 더하는데, 이때 자주 쓰는 게 구간 연산(interval arithmetic)이에요. 이게 뭐냐면 숫자 하나 대신 '이 값은 3.87과 3.88 사이'처럼 범위로 계산하는 방법이에요. 덕분에 부동소수점 오차까지 엄밀하게 관리할 수 있어요. 문제는 케이스가 수천, 수만 개로 불어나면 사람이 전부 검토할 수 없다는 거예요.
형식 증명: 컴퓨터가 채점하는 증명
여기서 Lean, Rocq(옛 이름 Coq), Isabelle 같은 증명 보조기(proof assistant)가 등장해요. 증명을 일종의 프로그래밍 언어로 쓰면, 컴파일러가 모든 논리 단계를 하나도 빠짐없이 검사해 줘요. 타입 체커가 깐깐한 채점관 역할을 하는 셈이죠. 4색 정리(2005년 Coq)나 케플러 추측(2014년 Flyspeck 프로젝트)처럼 컴퓨터 계산이 많이 들어간 증명들도 이렇게 형식화되면서 신뢰를 얻었어요.
최근에는 여기에 AI가 붙고 있어요. LLM이 증명 전략을 떠올리고 Lean 코드를 쓰면 Lean이 그걸 검증해요. AI가 그럴듯한 헛소리(환각)를 해도 Lean을 통과하지 못하니까, 생성은 AI가 하고 검증은 기계가 하는 조합이 되는 거죠. 이번 저장소에서 AI가 정확히 어느 부분을 도왔는지는 README와 증명 파일에서 직접 확인해 보세요.
그래도 꼭 확인해야 할 것들
형식 증명도 만능은 아니에요. 개발자 입장에서 Lean 증명을 볼 때 확인할 점이 있어요.
- 명제를 제대로 옮겼는지: 정의를 잘못 쓰면 엉뚱한 정리를 완벽하게 증명하게 돼요. 테스트는 통과했는데 테스트 자체가 틀린 상황과 똑같죠.
sorry가 남아 있는지: Lean에서 '이 부분은 일단 증명된 걸로 쳐줘'라는 뜻의 키워드예요.- 추가 공리나
native_decide를 썼는지: 계산을 컴파일된 코드로 돌리면 빠르지만, 그만큼 믿어야 하는 범위가 Lean 커널(검증의 핵심부) 밖으로 넓어져요.
#print axioms 정리이름 명령 하나면 증명이 어떤 공리에 기대는지 누구나 확인할 수 있어요.업계 맥락과 한국 개발자에게 주는 시사점
AI 수학은 빠르게 발전해 왔어요. DeepMind의 AlphaProof가 2024년 국제수학올림피아드(IMO)에서 은메달 수준을 기록했고, 2025년에는 여러 모델이 금메달 수준에 올랐죠. 이번 사례가 흥미로운 건 대형 연구소의 발표가 아니라 공개 저장소 형태로 나왔다는 점이에요. AI와 Lean만 있으면 오래된 난제에 도전하는 문턱이 확실히 낮아지고 있다는 신호예요.
형식 검증은 수학만의 이야기가 아니에요. AWS는 IAM 정책 검증에 자동 추론(automated reasoning)을 쓰고, seL4 마이크로커널은 구현이 명세대로 동작한다는 게 형식적으로 증명됐어요. 관심이 생겼다면 게임처럼 Lean을 배우는 'Natural Number Game'부터 시작해 보세요. '생성은 AI, 검증은 기계' 패턴은 당장 업무에도 쓸 수 있어요. AI가 짠 코드를 테스트, 타입 체크, 정적 분석에 통과시키는 거죠. 이런 검증 장치가 촘촘할수록 AI에게 맡길 수 있는 일도 많아져요.
마무리
AI는 아이디어를 내고, 기계는 검증하고, 사람은 무엇을 증명할지 정해요. 이번 증명이 수학계 검증을 통과할지는 지켜봐야 해요. 여러분은 어떻게 생각하세요? 컴퓨터만 끝까지 확인할 수 있는 증명을 우리가 '이해했다'고 말할 수 있을까요?
🔗 출처: Hacker News