수학 난제 열 개가 한꺼번에 풀렸다는 소식이 8월 초에 나왔습니다. 그런데 이 발표에서 정말 새로운 건 열 개라는 숫자가 아니에요.

증명이 기계가 읽는 형식으로 함께 공개됐다는 점입니다. 덕분에 이 글을 읽는 누구든 발표자를 믿지 않고도 결과를 직접 확인할 수 있습니다.

OpenAI가 공개한 253쪽 논문 표지 OpenAI가 공개한 253쪽 논문 표지 — 출처: OpenAI

8월 1일에 공개된 것

OpenAI는 아직 출시하지 않은 내부 모델이 수학과 이론 전산학에서 열 개의 결과를 만들어냈다고 발표했습니다. 각 문제는 최소 10년 이상 풀리지 않은 채 남아 있던 것들입니다.

논문 초록 — 내부 모델이 만든 결과라는 서술과 비소픽 군 항목 논문 초록 — 내부 모델이 만든 결과라는 서술과 비소픽 군 항목 — 출처: OpenAI

같이 공개된 자료가 넷입니다.

자료 분량 형태
본문 논문 253쪽 PDF
추론 과정 기록 62쪽 PDF
Lean 증명 코드 54만 줄 GitHub
독립 검증 설정 12건 GitHub

열 개를 모두 찾는 데 든 계산 비용은 약 280만 원(2,000달러)으로 집계됐습니다. 모델의 이름이 Astra로 함께 공개됐지만, 정작 논문 초록은 모델명을 쓰지 않고 an internal OpenAI model이라고만 적었습니다.

Lean 증명 저장소는 논문 공개 며칠 뒤 Apache-2.0 라이선스로 열렸고, 논문 본문도 8월 6일 자로 한 차례 수정을 거쳤습니다.

이 발표가 이전과 갈리는 지점

AI가 수학 문제를 풀었다는 발표는 전에도 있었습니다. 문제는 늘 그다음이었어요 — 그 증명이 맞는지 누가 확인하느냐는 것이죠.

증명 보조기가 하는 일

Lean은 증명 보조기(proof assistant)입니다. 수학의 정의와 논증을 프로그래밍 언어처럼 적어 넣으면, 논리적으로 빈 곳이 하나라도 있을 때 통과시키지 않습니다.

사람의 검토는 논증을 따라 읽으며 이상한 곳을 찾는 일이라 읽는 사람의 집중력과 시간에 달려 있습니다. Lean의 확인은 그렇지 않습니다. 전제에서 결론까지의 모든 단계가 규칙에 맞는지를 기계가 하나씩 대조하고, 한 군데라도 어긋나면 빌드가 실패합니다.

미완성 표시가 0이라는 뜻

Lean에는 sorry라는 표시가 있습니다. 아직 증명하지 못한 자리를 임시로 메워 두고 나머지를 먼저 짜맞출 때 쓰는 것으로, 이게 남아 있으면 증명은 완결된 게 아닙니다.

이 저장소의 sorry는 0개입니다. 실제로 받아서 세어 보면 걸리는 파일이 하나도 없습니다.

저장소를 받아 증명 규모와 미완성 표시를 직접 확인한 화면 저장소를 받아 증명 규모와 미완성 표시를 직접 확인한 화면 — 출처: 직접 실행

쓰인 공리도 propext, Classical.choice, Quot.sound 셋뿐입니다. 셋 다 표준 수학 라이브러리인 mathlib이 일상적으로 쓰는 것으로, 결과를 위해 따로 끌어들인 가정이 없다는 뜻입니다.

253쪽을 하루에 다 읽을 사람은 없지만, 기계는 전부 읽습니다

무엇을 풀었나

열 개 결과는 여덟 개 분야에 흩어져 있습니다. 한 사람이 전부를 심사할 수 있는 범위가 아니라는 점이 이번 발표의 성격을 그대로 보여줍니다.

비소픽 군의 존재를 증명한 3장 도입부 비소픽 군의 존재를 증명한 3장 도입부 — 출처: OpenAI

번호 분야 결과
1 기하 구 채우기 상계 확정
2 부호이론 이진·구면 부호 개선
3 군론 비소픽 군 존재 증명
4 작용소대수 Connes 강성 반례
5 회로복잡도 퍼머넌트 하계 강화
번호 분야 결과
6 양자정보 병렬 반복 정리 확장
7 격자암호 최근접 벡터 난해성
8 볼록기하 Ehrhart 부피 상계
9 조합론 다색 램지 수 하계
10 극단그래프 두 추측의 반례

대표 결과 하나 — 비소픽 군

군(group)은 대칭을 다루는 수학의 기본 구조입니다. 어떤 군이 소픽(sofic)하다는 건, 그 군의 곱셈표를 유한한 집합의 순열로 거의 그대로 흉내 낼 수 있다는 뜻이에요. 오차를 원하는 만큼 작게 줄일 수 있으면 소픽입니다.

모든 가산군이 소픽한가 — 1999년 Gromov의 논의에서 비롯된 이 물음은 27년 동안 답이 없었습니다. 이번에 나온 답은 아니오이고, 반례로 이진 Leavitt 대수의 단위군이 제시됐습니다.

나머지에서 눈에 띄는 것

구 채우기에서는 Cohn–Elkies 선형계획이 줄 수 있는 한계가 정확히 얼마인지가 확정됐습니다. 고차원에서 구를 얼마나 촘촘히 쌓을 수 있는지에 대한 상계인데, 이 방향의 일반 상계는 1978년 이후 크게 움직이지 않았던 자리입니다.

조합론 쪽 세 결과는 Erdős 문제 146번·180번·183번에 각각 답을 냈습니다. 램지 수 쪽은 세 색 이상에서 Rₖ(3)가 k의 Θ(k)제곱으로 자란다는 하계입니다.

계산 이론 쪽에서는 퍼머넌트를 계산하는 나눗셈 없는 회로에 Ω(n² log log n) 게이트, 수식에는 Ω(n⁴/log n) 잎이 필요하다는 하계가 나왔습니다.

한국이 쓰는 암호와 닿는 자리

일곱 번째 결과는 최근접 벡터 문제입니다. 격자 위에 촘촘히 놓인 점들 가운데 주어진 좌표에서 가장 가까운 점을 찾는 문제인데, 3SAT에서 직접 환원해 근사조차 어렵다는 하한을 강화했습니다.

이 대목이 한국과 닿습니다. 국가정보원이 주관한 양자내성암호 공모전 KpqC에서 최종 선정된 네 종 가운데 HAETAE·NTRU+·SMAUG-T 셋이 격자 문제의 어려움에 기대는 방식이고, 정부는 2023년 양자내성암호 전환 마스터플랜을 내놓은 상태예요.

방향을 뒤집어 읽지 않는 게 중요합니다. AI가 암호를 깬 게 아니라 암호가 딛고 선 어려움이 더 단단하다는 쪽으로 결과가 나왔습니다. 다만 이번 하한은 암호 설계가 실제로 쓰는 가정과 층위가 달라서, 우리가 쓰는 암호가 곧바로 더 안전해졌다고 옮기면 과장입니다.

직접 확인해 보는 방법

이 발표의 가장 실질적인 부분은 여기입니다. 저장소를 받아 빌드하면 열 개 증명이 전부 통과하는지 각자 확인할 수 있어요.

🔗 링크 첨부 - https://github.com/openai/ten-proofs

결과별 Lean 증명 코드 줄 수 결과별 Lean 증명 코드 줄 수 — 출처: 직접 작성 (자료: openai/ten-proofs)

필요한 건 Lean 설치 도구인 elan 하나입니다. 저장소를 받은 뒤 lake exe cache get으로 mathlib 캐시를 내려받고 lake build All을 돌리면 열 개가 모두 검증됩니다. 하나만 확인하고 싶으면 모듈 이름을 붙여 lake build SpherePacking처럼 돌리면 됩니다.

증명 코드는 전부 합쳐 54만 8,215줄입니다. 가장 긴 최근접 벡터 문제가 13만 줄, 가장 짧은 다색 램지 수가 3천 줄로 40배 넘게 차이가 납니다.

저장소에는 Comparator 챌린지 설정 12건도 들어 있습니다. Lean 본체와 독립된 외부 검사기로 같은 증명을 다시 확인하도록 만든 장치예요. 검증 도구 자체를 못 믿겠다는 반론까지 미리 받아 둔 셈입니다.

그래도 남는 물음

여기까지가 확인되는 부분이고, 확인되지 않는 부분도 분명합니다.

기계가 증명을 한 단계씩 대조하는 개념 컷 기계가 증명을 한 단계씩 대조하는 개념 컷 — 출처: 논문 공개 자료 기반 자가 생성

사람이 어디까지 개입했나

OpenAI는 연구원들이 원고를 준비하고 증명을 Lean으로 옮겼으며 정확성에 대한 책임도 자신들에게 있다고 밝혔습니다. 다만 수학적 논증 자체는 모델에게서 나왔다는 게 회사의 설명입니다. 이 경계선을 어떻게 읽느냐에 따라 평가가 갈립니다.

형식검증이 보장하지 않는 것

Lean이 확인해 주는 건 적어 넣은 문장이 참이라는 사실입니다. 그 문장이 원래 풀려던 문제를 제대로 옮긴 것인지, 그 결과가 분야에서 중요한지는 여전히 사람이 판단할 몫입니다. 형식화가 동료평가를 대신하지는 못합니다.

반응과 검증은 다르다

Fields 메달 수상자 Timothy Gowers는 결과 하나를 주저 없이 최상위 저널에 추천하겠다고 말했고, Erdős 문제 목록을 관리하는 Thomas Bloom은 이번 결과가 큰 뉴스라고 평했습니다. 다만 Bloom은 AI가 수학자를 대체한다는 해석에는 선을 그으며, 이 작업이 백 년 넘게 쌓인 수학 이론 위에 서 있다고 덧붙였습니다.

발표 당일에 나온 이런 반응들은 아직 검증이 아니라 첫인상입니다. 여덟 개 분야에 걸친 253쪽을 하루 만에 읽은 사람은 없으니까요. OpenAI 연구원 Noam Brown도 밀레니엄 문제 같은 더 큰 난제에는 도전했다가 실패했다고 밝혔습니다.

모델은 여전히 닫혀 있다

Astra는 공개되지 않았습니다. 외부에서 같은 실험을 재현할 수 없고, 학습 데이터나 방법도 알려지지 않았습니다. 확인 가능한 것은 결과물뿐입니다.

검증할 수 있는 결과와 검증할 수 없는 과정이 한 발표에 같이 들어 있습니다

정리하면

이번 발표에서 되풀이해 볼 만한 것은 열 개라는 숫자보다 형식입니다. 주장과 함께 기계가 확인할 수 있는 증거를 붙였고, 그 증거는 발표자의 권위와 무관하게 각자 돌려 볼 수 있습니다.

AI가 만든 결과를 어떻게 신뢰할 것인가라는 물음에 지금까지 나온 답 중에서는 가장 구체적인 형태예요. 수학은 이걸 할 수 있는 몇 안 되는 분야이기도 하고요.

참고 출처