2026년 8월 1일, OpenAI 공식 웹사이트에 화려한 시연 영상이나 그래픽도 없이 공지 하나가 올라왔습니다. 자신들의 차세대 핵심 모델인 내부용 Astra가 수학과 이론 컴퓨터 과학의 난제 10개를 한꺼번에 해결했다는 소식이었습니다. 이 문제들 중 일부는 수십 년 동안 방치되어 여러 세대의 수학자들이 도전했다가 실패했으며, 일부는 튜링상 수상자조차 해결하지 못했던 난제였습니다. 공지가 올라온 지 24시간 만에 Hacker News에는 600개가 넘는 토론 댓글이 달렸습니다. 필자를 가장 놀라게 한 것은 바로 숫자였습니다. OpenAI는 이 10개 문제를 푸는 데 들어간 총 추론 비용이 약 2,000달러에 불과하다고 밝혔습니다.
2,000달러라는 액수는 어떤 의미일까요? 수학 박사과정 학생의 한 달 수당보다도 적은 금액입니다. 이는 수학 연구의 시행착오 비용이 ‘인년(person-years)’ 단위에서 ‘달러’ 단위로 전환되고 있음을 의미합니다. 다만 이 금액은 공개 API 가격 기준으로 산정한 추론 비용일 뿐이며, 모델 사전 학습에 들어간 천문학적인 투자 비용은 포함되지 않았습니다. 또한 Astra가 성공하기까지 얼마나 많은 실패를 겪었는지도 알려지지 않았습니다. 이 두 가지 점에 대해서는 뒤에서 자세히 설명하겠습니다.
그림: OpenAI 공식 웹사이트에 게시된 10가지 수학 성과 커버 이미지. 출처: openai.com
수학 난제가 그토록 어려웠던 이유
우선 이번에 해결된 문제들의 무게감을 살펴보겠습니다. 10개 문제는 고차원 기하학, 부호 이론, 군론, 양자 컴퓨팅, 암호학, 그래프 이론 등 다양한 분야에 걸쳐 있습니다. 그중 세 가지를 예로 들어보겠습니다.
“비-sofic 군(non-sofic group)이 존재하는가?” — 군론 분야의 핵심 미해결 과제로, 학계에서는 존재할 것이라 널리 믿었지만 20년이 넘도록 아무도 실제로 구현해내지 못했습니다. “최단 벡터 문제(SVP)“의 근사 난이도 — 암호학계가 3~40년 동안 주시해 온 문제로, 양자 컴퓨터 시대에 어떤 암호 체계를 사용할지와 직결됩니다. “다색 램지 수”의 하한선 — 전설적인 수학자 폴 에르되시(Paul Erdős)의 상금 문제 목록 183번에 해당하는 문제로, 그는 평생 1,000개가 넘는 난제에 상금을 걸었습니다.
왜 이 문제들은 이토록 어려울까요? 수학적 증명은 미로 속에서 출구를 찾는 것과 같습니다. 모든 단계마다 명확한 논리적 근거가 필요하며, 한 걸음이라도 틀리면 이전의 모든 작업이 무용지물이 됩니다. 일반 시험은 정답지라도 있지만, 수학 난제에는 정답지가 없습니다. 출구가 어디에 있는지, 심지어 출구가 존재하는지조차 아무도 모릅니다. 인간 수학자는 직관, 경험, 운에 의존해 한 번에 하나의 경로만 탐색할 수 있습니다.
또 다른 어려움도 있습니다. 이런 난제들은 ‘첫 번째 아이디어의 방향’에서 막힙니다. 논증의 출발점이 틀리면 뒤이어 아무리 정교한 기법을 써도 소용없습니다. 수세대의 수학자들이 수십 년 동안 얼마나 많은 잘못된 방향을 배제해왔는지는 아무도 집계하지 못했지만, 그 모든 방향 뒤에는 실제 인간의 수많은 시간이 들어갔습니다.
AI는 어떻게 난제를 풀었나
OpenAI의 접근 방식은 한 문장으로 요약할 수 있습니다. 모델이 스스로 수천, 수만 개의 ‘초안 증명’을 생성하게 한 뒤, 기계를 통해 하나씩 검증하는 것입니다.
여기서 핵심 역할을 한 것이 바로 Lean입니다. Lean은 형식 검증 도구로, 철저하고 공정한 시험 감독관과 같습니다. 증명을 Lean이 이해할 수 있는 형식으로 작성하면 라인별로 논리를 검사하여 맞으면 통과, 틀리면 즉시 기각합니다. 사적인 감정이나 융통성이 개입할 여지는 없습니다. AI 학습 과정에서 Lean의 검증을 통과한 논증은 보상을 받게 되었고, 이를 통해 모델은 ‘검증 가능한 올바른 논증을 작성하는 법’을 습득했습니다. 지난 2년간 AI의 수학 능력이 급상승한 것은 바로 이 자동 채점기 덕분입니다. 수학은 정답과 오답을 완벽하고 객관적으로 판정할 수 있는 몇 안 되는 분야입니다. 글쓰기나 프로그래밍에서는 어렵지만, 수학에서는 가능합니다.
10만 개의 분신이 동시에 미로 속에 들어가는 모습을 상상해 보세요. 대다수는 벽에 부딪혀 막히지만, 극소수는 출구에 도달합니다. 감독관은 출구에 도달한 경로만을 인정합니다. 인간은 한 번에 하나의 길만 갈 수 있지만, AI는 동시에 1만 개의 경로를 시도할 수 있습니다. 이는 차원이 다른 규모의 차이입니다.
이번 성과의 구체적 과정은 다음과 같습니다. 내부용 Astra 모델이 방대한 후보 논증을 생성하면 Lean이 유효한 논증을 걸러냅니다. 이후 연구진이 검증된 논증을 논문 형태로 정리하고, 모델이 다시 각 단계를 형식화하여 기계가 재검증할 수 있도록 했습니다. OpenAI는 모델이 자신의 사고 과정을 서술한 기록도 공개했습니다. 10개 문제 모두 해결되었으며, 소모된 총 토큰 비용은 약 2,000달러였습니다.
일반인에게도 중요한 이유
첫째, AI가 처음으로 ‘인간이 작성한 적 없는 새로운 해답’을 제출했습니다. OpenAI에 따르면 이 문제들의 핵심 연구 결과는 최소 10년 동안 실질적인 진전이 없었습니다. 과거 AI가 보여준 수학 능력은 주로 문제 풀이, 경시대회, 기존 정리의 복현에 머물렀으나, 이번에는 수십 년간 미해결 상태였던 실제 난제를 해결한 것입니다.
둘째, 수학은 기술의 상류에 위치합니다. 최단 벡터 문제는 후-양자 암호학과 관련이 있고, 구 채우기 및 부호 이론은 통신과 데이터 저장 기술에 직결됩니다. 수학적 기반이 한 걸음 앞서 나가면, 그 위의 엔지니어링 기술도 조만간 따라가게 됩니다.
셋째, 비용 곡선이 변했습니다. 수학자 테렌스 타오(Terence Tao)는 올해 ‘빅 매스(Big Math)’ 개념을 제안했습니다. 인간이 창의적인 방향을 제시하고 AI가 번거로운 작업을 수행하는 방식입니다. 2,000달러라는 비용은 과거 최고 연구팀만 수행할 수 있었던 방대한 대규모 탐색을 이제 개인 연구자도 시도할 수 있게 되었음을 의미합니다. 올해 5월 OpenAI가 AI를 활용해 에르되시의 단위 거리 추측을 반박한 이후, 최소 5편의 인간 논문이 이 방향을 이어서 연구를 진행했습니다. AI의 성과물이 인간 연구의 새로운 출발점이 되고 있는 것입니다.
일반 사용자들에게 가장 직접적인 신호는 AI가 ‘인간이 쓰지 않은 새로운 정리’를 만들어낼 수 있다는 사실입니다. 이는 AI가 단지 ‘본 것을 재진술하는 수준’에서 점점 멀어지고 있음을 뜻합니다. 이러한 능력은 수학 분야에만 머물지 않고 조만간 엔지니어링과 기술 개발로 흘러들어갈 것이며, 결국 우리가 사용하는 스마트폰과 서비스에 반영될 것입니다.
낙관파 vs 회의파: 누구의 주장이 더 타당한가
Hacker News 토론장에서는 두 진영이 팽팽하게 대립했습니다.
| 입장 | 핵심 주장 |
|---|---|
| 낙관파 | 결과가 실제 존재하고 검증 가능함. Lean 형식화를 통해 조작이나 환각의 여지가 극히 적음. 한 학생이 이 중 몇 문제만 풀어냈더라도 필즈상 후보로 거론되었을 수준임. 이는 1997년 딥블루가 카스파로프를 꺾었던 순간의 수학 버전임. |
| 회의파 | ’초대형 탐색 공간 + 자동 검증’에 의존한 단순 무력(brute force)일 수 있으며 새로운 개념적 통찰을 창출하지 못함. OpenAI는 프롬프트나 실패 횟수를 공개하지 않았음. 기술적 진보가 S-곡선인지 지수 곡선인지에 대한 논쟁 — 발전은 로켓 탑승보다 등산에 가까울 수 있음. 이런 발표에는 마케팅 동기가 포함되어 있어 공표된 주장과 증거 사이에 비공개 세부사항이 존재함. 1976년 컴퓨터가 4색 정리를 검증했을 때도 수학자들에게 거부감을 주었지만 학문의 본질을 바꾸지는 못했음. |
양쪽 모두 타당한 근거를 가지고 있습니다. 회의파의 가장 강력한 지적은 한 Hacker News 유저로부터 나왔습니다. “Lean은 ‘올바르게 작성된 명제’만을 증명할 수 있을 뿐, 명제 자체가 문제의 본질을 제대로 반영하고 있는지는 인간이 확인해야 한다”는 점입니다. 기계는 추론 과정을 검증할 뿐 문제 자체를 깊이 이해했는지는 책임지지 않습니다. 낙관파의 반론은 간단합니다. 4색 정리 검증 이후 그것은 정리가 되었고, 지난 50년 동안 아무도 이를 뒤집지 못했습니다.
시사점
수학자 공동체의 반응은 극명하게 엇갈렸습니다. 누군가는 “수학의 어두운 밤”이라며 장문의 글을 남겼고, 누군가는 수학이 대중에게 한 걸음 더 다가가는 계기가 될 것이라 보았습니다. OpenAI는 이례적으로 수학계의 ‘라이덴 선언’을 인용하며 논쟁이 존재함을 인정하고, 증명 과정과 형식화 코드, 사고 과정 기록을 공개하기로 결정했습니다. 이러한 투명성은 AI 기업 사이에서 매우 드문 일입니다.
AI가 수학자를 대체할지 예측하는 것은 본질이 아닙니다. 확인할 수 있는 사실은 세 가지입니다. 10개의 난제가 실제로 해결되었고 Lean으로 검증 가능하다는 점, 비용이 2,000달러 수준이라는 점, 그리고 논쟁이 이제 막 시작되었다는 점입니다. 필자의 입장은 명확합니다. ‘증명의 성립 여부’는 기계와 동료 평가(peer review)에 맡기고, ‘AI가 수학을 참되게 이해하는가’는 시간에 맡기는 것입니다. AI가 ‘진정으로 수학을 이해하는가’는 철학적 질문에 가까우며, 시간이 그 답을 줄 것입니다.
참고 링크:
- OpenAI: Ten advances in mathematics
- HN 토론 (item?id=49157930)
