오픈AI는 2026년 8월 1일 미공개 차기 모델 아스트라(Astra)의 내부 판본이 최소 10년 이상 주요 결과에 진전이 없던 수학·이론전산학 난제 10건의 새 결과를 만들어냈다고 공개했다. 대상 문제는 고차원 기하, 부호이론, 산술회로 복잡도, 군론, 작용소대수, 양자 복잡도, 격자 암호, 극단 조합론에 걸쳐 있다. 오픈AI는 이 해답들을 찾는 데 필요한 토큰 총량이 GPT-5.6 Sol API 요금으로 환산하면 약 2,000달러 수준이라고 밝혔고, 모델이 만든 논증을 사람이 같은 모델을 써서 논문 형태로 다듬은 뒤 모델이 각 논증을 Lean 증명서로 형식화했다고 설명했다. ASAP은 오픈AI 공식 발표를 1차 출처로 무엇이 새로 풀렸고 무엇이 여전히 사람 몫으로 남았는지 정리한다.

열 개의 결과는 한 분야가 아니라 여덟 갈래에서 나왔다

오픈AI가 공개한 결과 10건은 서로 다른 수학 하위 분야에 흩어져 있으며, 모두 주요 결과에 최소 10년, 대부분은 그보다 훨씬 오래 진전이 없던 문제다. 목록을 오픈AI 발표 그대로 정리하면 다음과 같다.

첫째, 고차원 구 채우기(sphere packing)에서 채우기 밀도의 새로운 상한을 콘-엘키스(Cohn-Elkies) 한계까지 낮췄다. 둘째, 이진 부호와 구면 부호에서 정해진 최소 거리에 대해 이진 부호의 최대 크기 한계를 지수적으로 개선했고 고차원 구면 부호에도 같은 계열의 결과를 얻었다. 셋째, 비소픽 군(non-sofic group)의 존재를 확립하는 구성을 제시해 군론의 중심 미해결 문제 하나에 답했다. 넷째, 특정 군이 그 폰 노이만 대수로 유일하게 결정된다는 콘느(Connes) 강직성 추측을 반증했다.

다섯째, 산술회로 복잡도에서 퍼머넌트(permanent) 계산에 대한 새 하한을 얻었고 여기에는 n⁴/log n 규모의 산술 공식 하한이 포함된다. 여섯째, 일반적인 2인 양자 게임에 대한 지수적 병렬 반복 정리를 세워 고전 복잡도 이론의 기초 원리를 양자 영역으로 확장했다. 일곱째, 양자 이후 암호와 직결되는 격자 문제인 최근접 벡터 문제(closest vector problem)의 다항 인자 근사 난해성을 보였다. 여덟째, 내부 격자점이 무게중심 하나뿐인 볼록체의 최대 부피를 모든 차원에서 결정해 에르하르트(Ehrhart) 부피 추측을 다뤘다. 아홉째, 다색 삼각형 램지 수의 초지수적 하한을 세워 에르되시 문제 183번을 해결했다. 열째, 극단 그래프 이론의 컴팩트성 추측과 축퇴성 추측에 대한 결과로 에르되시 문제 146번과 180번을 해결했다.

모델이 한 일과 사람이 한 일의 경계는 발표문에 명시돼 있다

오픈AI는 작업 분담을 흐리지 않고 세 단계로 나눠 적었다. 수학적 논증 자체는 아스트라의 내부 판본이 생성했고, 사람이 같은 모델을 도구로 써서 그 논증을 원고로 준비했으며, 그 뒤 모델이 각 논증을 Lean 증명서로 형식화했다. 오픈AI는 원고 준비와 Lean 형식화에 자사가 관여했으며 결과의 정확성에 대한 책임은 자사가 진다고 밝혔다. 여기에 더해 각 해답마다 모델이 스스로의 사고 과정을 서술한 기록을 함께 공개했다.

이번 발표에는 전사가 있다. 오픈AI는 2026년 5월 미공개 모델을 평가하던 중 에르되시 단위거리 추측을 반증하는 결과를 얻어 공개한 바 있고, 그 결과가 이후 수학과 이론전산학의 후속 연구를 촉발했다고 밝혔다. 발표문 각주에는 합-곱 추측이 실수에서 성립하지 않음을 보인 블룸·소인·실드크라우트·젤레조프의 논문을 비롯해 다섯 편의 후속 연구가 열거돼 있다. 접근성 측면의 배경도 함께 제시됐다. 오픈AI는 과학자와 수학자 10만 명에게 자사 최고 모델을 무료로 제공하는 ChatGPT for Academic Researchers를 최근 시작했다고 밝혔다.

2,000달러라는 숫자를 곧이곧대로 읽으면 안 되는 이유

약 2,000달러라는 금액은 이번 발표에서 가장 많이 인용될 숫자이지만, 이 값이 무엇을 재고 무엇을 재지 않는지 구분해야 한다. 오픈AI의 서술은 이 문제들의 해답을 찾는 데 필요한 토큰 총량을 Sol API 요금으로 환산한 값이다. 즉 성공한 탐색의 토큰 비용이며, 원고 작성에 투입된 사람의 시간, Lean 형식화 과정에서 든 추가 연산, 그리고 이번에 공개되지 않은 실패한 시도들의 비용은 이 숫자에 포함된다고 명시되지 않았다.

동시에 이 숫자를 과소평가하는 것도 정확하지 않다. GPT-5.6 Sol의 API 요금은 2026년 7월 30일 기준 100만 토큰당 입력 5달러, 출력 30달러다. 2,000달러는 이 요금 체계에서 대략 수천만 토큰 수준의 연산에 해당한다. 10년 이상 정체된 문제 열 개의 해답을 찾는 탐색이 개인 연구자의 한 해 클라우드 예산에도 못 미치는 규모의 연산으로 끝났다는 뜻이다. 비용의 절대값이 작다는 사실보다 중요한 것은 비용의 단위가 바뀌었다는 점이다. 난제 해결의 병목이 연산 예산에서 문제 선택과 검증으로 옮겨가면, 어떤 문제를 물을지 아는 사람의 가치는 떨어지는 것이 아니라 올라간다.

한 가지 더 짚어야 할 것은 이 숫자가 아스트라의 요금이 아니라는 점이다. 결과를 낸 것은 아스트라의 내부 판본이고, 환산 기준은 현재 판매 중인 Sol의 요금이다. 아스트라가 실제로 출시될 때 어떤 가격과 어떤 처리량으로 제공될지는 이번 발표에 없다. 2,000달러는 재현 비용의 상한이나 하한이 아니라 규모를 가늠하게 하는 환산치로 읽는 편이 정확하다.

Lean 증명서는 검증 부담을 없앤 것이 아니라 위치를 옮겼다

AI가 만든 수학 결과에서 지금까지 가장 큰 마찰은 검증이었다. 그럴듯하지만 어딘가 어긋난 긴 논증을 사람이 한 줄씩 따라가야 했고, 이 부담 때문에 주장의 양이 늘수록 학계의 확인 속도가 뒤처졌다. Lean 형식화는 이 지점을 정면으로 건드린다. 형식 증명이 통과하면 논증의 각 단계가 명시된 공리계 안에서 실제로 이어진다는 사실은 기계가 보증하고, 사람이 다시 검산할 필요가 없다.

다만 형식화가 보증하는 범위는 좁고 분명하다. Lean이 확인해주는 것은 진술 A로부터 진술 B가 따라 나온다는 사실이지, 진술 A와 B가 수학자들이 실제로 묻던 그 문제를 옳게 옮겨 적은 것인지는 확인해주지 않는다. 형식화된 정리문이 원래 추측의 정확한 번역인지, 정의가 표준적인지, 가정이 슬그머니 강해지지 않았는지는 여전히 사람이 읽어야 한다. 검증 노동이 사라진 것이 아니라 논증 전체에서 정리문과 정의라는 훨씬 짧은 구간으로 압축된 것이다.

그래서 이번 공개에서 실질적으로 중요한 것은 열 개의 결과 자체보다 각 결과에 Lean 증명서와 사고 과정 서술이 붙어 있다는 구성이다. 결과만 던지면 학계는 진위 확인에 시간을 쓰지만, 증명서가 붙으면 논쟁의 초점이 옳은가에서 무엇을 의미하는가로 곧장 넘어간다. 오픈AI가 수학 공동체에 결과를 맥락 속에 놓아달라고 요청한 것도 이 구조를 전제한 주문으로 읽힌다.

회사가 스스로 저자 표기를 좁힌 선언은 이례적이다

오픈AI는 발표문에서 저자 표기 원칙을 분명히 밝혔다. AI 시스템이 전부 생성한 증명에 대해 사람의 저작을 주장하는 것은 시스템의 기여와 진짜 사람의 지적 작업 양쪽을 왜곡한다는 것이다. 자사는 원고 준비와 Lean 형식화를 도왔고 정확성에 책임을 지되, 수학적 논증 자체는 자사 시스템이 생성했다고 적었다. 아울러 AI와 수학에 관한 라이덴 선언(Leiden declaration)에 서명한 이들을 포함해 AI의 영향을 우려하는 쪽에 깊은 존중과 이해를 표한다고 밝혔다.

이 대목이 이례적인 이유는 방향 때문이다. 기술 회사가 자사 시스템의 역할을 축소해 논란을 피하는 선택이 흔한데, 여기서는 반대로 사람이 저자로 이름을 올리는 관행을 스스로 제한하자고 제안하고 있다. 이 원칙을 실제로 적용하면 마찰이 생기는 곳은 회사가 아니라 학계다. 논문의 저자란은 채용과 승진, 연구비 심사의 단위이고, 학술지는 지금까지 AI를 저자로 인정하지 않는 방향으로 정책을 정리해왔다. 논증을 생성한 주체를 저자로 적을 수 없고 사람이 저자를 주장해서도 안 된다면, 이 결과들은 기존 심사 체계 안에서 어디에 놓이는지가 문제로 남는다.

또 하나 눈여겨볼 것은 라이덴 선언을 언급한 방식이다. 오픈AI는 자사 입장을 밝히면서도 반대 견해를 반박 대상이 아니라 존중 대상으로 놓았다. 결과 공개와 규범 논의를 같은 문서 안에서 함께 진행하겠다는 태도이며, 수학계가 이번 결과를 어떻게 받아들일지는 결과의 옳고 그름과 별개로 이 규범 협상의 진행에 달려 있다.

국내 연구실과 기업이 지금 조정할 것

한국의 연구 현장에서 이번 발표가 곧바로 바꾸는 것은 연구 주제 선정의 셈법이다. 오랫동안 정체된 문제에 사람의 시간을 얼마나 투입할지 결정할 때, 이제는 최신 추론 모델로 먼저 며칠을 태워보는 선택지가 비용상 합리적인 범위에 들어왔다. 성공을 기대해서가 아니라, 실패해도 잃는 것이 연산비 정도이고 성공하면 선점 효과가 크기 때문이다. 특히 이번 목록에 격자 암호의 최근접 벡터 문제가 들어 있다는 점은 양자 이후 암호 전환을 준비하는 국내 보안 조직이 남의 일로 넘기기 어려운 대목이다. 격자 문제의 난해성 결과는 표준화 논의의 안전성 근거와 맞닿아 있다.

기업 쪽에서는 검증 인프라가 실질적인 격차 요인이 된다. 모델이 생성한 논증이나 설계를 형식 도구로 확인하는 체계를 갖춘 조직과 그렇지 않은 조직은, 같은 모델을 써도 결과를 신뢰 가능한 산출물로 바꾸는 속도가 다르다. Lean 같은 증명 보조기는 수학에만 쓰이는 도구가 아니라 알고리즘과 프로토콜의 정확성 검증에도 쓰인다. 모델 도입 예산을 짤 때 생성 쪽에만 배분하고 검증 쪽을 비워두는 구성은 이번 사례가 보여준 작업 분담과 어긋난다.

아직 답이 없는 것들

첫째는 성공률이다. 오픈AI는 열 개의 결과를 선별해 공개했다고 밝혔을 뿐, 몇 개의 문제에 도전해 몇 개를 풀었는지는 밝히지 않았다. 선별된 성공 사례만으로는 이 능력이 임의의 미해결 문제에 얼마나 일반적으로 작동하는지 판단할 수 없다. 2,000달러라는 비용의 의미도 이 분모가 나와야 확정된다.

둘째는 독립 검토다. Lean 증명서가 붙어 있어도 정리문이 원래 추측을 옳게 옮겼는지, 결과가 각 분야에서 얼마나 중요한지는 해당 공동체의 판단 영역이다. 오픈AI 스스로 수학 공동체가 결과에 깊이 관여하고 맥락 속에 놓아주기를 바란다고 적었다. 지금까지 나온 것은 발표와 자료이며, 분야별 평가는 앞으로의 일이다.

셋째는 아스트라 자체다. 결과를 낸 것은 차기 주요 모델의 내부 판본이고, 이 모델의 사양과 공개 시점, 접근 조건은 이번 발표에 없다. 같은 능력을 외부 연구자가 언제 어떤 조건으로 쓸 수 있는지가 정해지기 전까지, 이번 결과는 도구의 확산이 아니라 도구의 상한을 보여주는 기록으로 남는다.

출처: 오픈AI 공식 발표 "Ten advances in mathematics and theoretical computer science"(2026년 8월 1일) 및 오픈AI API 요금 페이지 기반 ASAP 정리