3줄 요약

  1. OpenAI가 2026년 7월 29일 공개한 발표 글이다. 차기 주력 모델 Astra의 내부 버전이, 10년 넘게(대부분은 훨씬 더 오래) 주요 결과에 진전이 없던 수학과 이론전산학 난제 10건에 새 결과를 냈다고 밝혔다.
  2. 대상은 고차원 기하, 부호이론, 산술회로 복잡도, 군론, 작용소 대수, 양자 복잡도, 격자 암호, 극단 조합론에 걸친다. 해를 찾는 데 든 토큰 비용은 Sol API 요율로 약 2,000달러였고, 각 논증은 사람이 원고로 정리한 뒤 모델이 Lean 인증서로 형식화했다.
  3. OpenAI는 AI가 전부 생성한 증명을 사람의 저작으로 내세우는 것은 부정확하다는 귀속 원칙을 밝혔다. 원고 작성과 Lean 형식화, 정확성에 대한 책임은 자신들이 지되, 수학적 논증 자체는 시스템이 생성했다고 명시한다.

배경: Erdős 반증에서 열 건으로

OpenAI는 지난 5월, 미공개 모델을 평가하던 중 발견한 Erdős 단위거리 추측의 AI 생성 반증을 공개한 바 있다. 그 작업은 이미 수학과 이론전산학의 후속 전개를 촉발했다고 한다. OpenAI는 이런 흐름의 연장선에서, 과학자와 수학자 10만 명에게 최상위 ChatGPT 모델을 무료로 제공하는 ChatGPT for Academic Researchers도 최근 시작했다고 소개한다.

이번 발표는 개별 반증 한 건이 아니라, 열 개의 결과를 한 번에 내놓았다는 점이 다르다. 선정 기준은 명확하다. “최소 10년 이상, 대부분은 그보다 훨씬 오래 주요 결과에 진전이 없던” 문제들이다. OpenAI는 이 문제들이 각 분야에서 상당한 관심을 받아 왔으며, 그중 여럿은 수학 전반에 걸쳐 넓은 관심사라고 설명한다.

방법: Astra, 토큰 2천 달러어치, Lean 인증서

결과를 낸 주체는 차기 주력 모델 Astra의 내부 버전이다. OpenAI는 작업 방식을 이렇게 정리한다.

이 문제들의 해를 찾는 데 필요한 총 토큰 수는 Sol API 요율로 대략 2,000달러어치였다. 이 논증들은 같은 모델을 쓴 사람들이 원고로 정리했다. 이후 모델이 각 논증을 Lean 인증서로 형식화했다.

세 단계가 분리돼 있다. 모델이 논증을 생성하고, 사람이 그것을 원고로 다듬고, 다시 모델이 Lean으로 형식 증명을 만든다. 형식화한 인증서는 github.com/openai/ten-proofs 저장소로 공개했고, 각 해에 대해 모델이 스스로 사고 과정을 서술한 내레이션도 함께 내놓았다.

저장소를 직접 열어 보면, 결과별 Lean 파일 하나씩과 정리 목록을 담은 formalization.yaml이 있다. 코드와 극단 조합론이 각각 두 정리로 나뉘어 주 정리는 모두 열두 개인데, 열두 개 전부 미완성 표시(sorry)가 0건이고 propext, Classical.choice, Quot.sound라는 표준 공리 셋만 쓴다. Lean 4.32와 mathlib 위에서 형식화했으며, Comparator라는 독립 검사 도구로 증명을 다시 확인할 수 있게 해 뒀다. 형식화 자체는 Codex 프레임워크로 약 일주일이 걸렸다고 적혀 있다.

열 가지 결과

OpenAI가 새 결과를 제시한 문제 목록은 다음과 같다. 원문의 순서와 분야를 그대로 옮기되, 각 항목의 뒷문장은 공개된 Lean 인증서의 주 정리에서 확인한 더 구체적인 진술이다.

  1. 고차원 구 채우기 (High-dimensional sphere packing). Cohn-Elkies 문턱까지 내려가는 구 채우기 밀도의 새로운 상계. 형식 증명은 Cohn-Elkies 선형계획 한계에 도달하는 점근 상계를, 지수적으로 사라지는 오차항까지 붙여 확립한다.
  2. 이진 부호와 구면 부호 (Binary and spherical codes). 임의로 정한 최소 거리에서 이진 부호의 최대 크기에 대해 지수적으로 개선된 한계. 고차원 구면 부호에도 같은 방식의 결과. 핵심은 1977년 이래 최선이던 MRRW 한계를 0과 1/2 사이 모든 최소 거리에서 엄격히 밑돈다는 것이고, 구면 부호에서는 개선된 한계들의 위계를 세운다.
  3. 비-소픽 군 (Non-sofic groups). 비-소픽 군의 존재를 확립하는 구성. 군론의 핵심 미해결 문제를 다뤘다. 구성한 군이 유한 표현(finitely presented) 군이라는 점이 핵심이다. 모든 군이 유한 순열로 근사되느냐는 물음에 아니라고 답한 셈이다.
  4. Connes 강성 추측 (Connes’s rigidity conjecture). 특정 군이 그 폰 노이만 대수로 유일하게 결정된다는 오랜 추측을 반증. 반례는 서로 동형이 아닌 성질 (T) ICC 군을 무한히 많이 만들면서도, 그 군 폰 노이만 인자는 모두 동형이 되도록 한다.
  5. 산술회로 복잡도 (Arithmetic circuit complexity). permanent를 산술회로와 공식으로 계산하는 문제의 새 하한. 차수 n⁴/log n 규모의 산술공식 하한을 포함한다. 나눗셈을 허용한 유리식에서도 하한이 성립해, n이 32 이상이면 permanent를 계산하는 임의의 유리식은 변수 잎이 n⁴/(192 log₂ n) 규모 이상 필요하다.
  6. 양자 병렬 반복 (Quantum parallel repetition). 일반적인 2인 양자 게임에 대한 지수적 병렬 반복 정리. 고전 복잡도 이론의 기초 원리를 확장했다. 임의의 유한 2인 양자 게임에 대해 균일한 지수적 감소를 준다는 것이 형식화된 진술이다.
  7. 최근접 벡터 문제 (Closest vector problem). 최근접 벡터 문제에 대한 다항식 인자 근사 난해성. 포스트양자 암호와 연결된 기초 격자 문제다. 형식화는 근사 인자 400의 GapCVP가 무조건적으로 NP-난해임을 보이고, 같은 틀을 이진 최근접 부호어와 신드롬 복호의 NP-난해성으로도 확장한다.
  8. Ehrhart 부피 추측 (Ehrhart’s volume conjecture). 무게중심이 유일한 내부 격자점인 볼록체의 최대 부피를 모든 차원에서 결정. 모든 차원에서 그 상계가 날카롭다는(sharp) 부피 부등식으로 형식화됐다.
  9. 다색 램지 수 (Multicolor Ramsey numbers). 다색 삼각형 램지 수의 초지수적 하한. Erdős 문제 183을 해결했다. 명시적 하한이라, k가 2 이상일 때 삼각형 램지 수 R(k)가 ((1/(6·e³⁸))·k^(1/3)/ln k)^k 이상이고, 그 k제곱근이 무한대로 발산해 초지수적임을 보인다.
  10. 극단 수 추측 (Extremal number conjectures). 극단 그래프이론의 컴팩트성과 축퇴성(degeneracy) 추측을 각각 반례로 무너뜨렸다. Erdős 문제 146과 180을 해결했다. 하나는 Erdős–Simonovits 컴팩트성 추측의 정량적 반례이고, 다른 하나는 2-축퇴 이분 그래프에 대한 반례다.

수학 공동체에 대한 책임

발표 글의 마지막 절은 결과 목록이 아니라 태도에 관한 것이다. OpenAI는 수학 연구에 기여할 수 있는 시스템의 등장이 기술 회사 혼자 답할 수 없는 물음을 던진다고 인정하며, AI와 수학에 관한 Leiden 선언에 서명한 이들을 포함해 그 영향을 우려하는 쪽에 깊은 존중을 표한다고 적었다.

핵심은 귀속(attribution)의 정직성이다.

우리는 귀속이 결과가 어떻게 만들어졌는지를 정직하게 반영해야 한다고 믿는다. AI 시스템이 전적으로 생성한 증명에 인간 저작권을 주장하는 것은, 그 시스템의 기여와 진정한 인간 지적 노동의 본질을 모두 왜곡하는 일이다.

OpenAI는 원고를 준비하고 증명을 Lean으로 형식화하는 일을 도왔으며 그 정확성에는 책임을 지지만, 수학적 논증 자체는 시스템이 생성한 것이라고 선을 그었다. 그러면서 수학 공동체가 이 결과들을 깊이 다뤄 맥락 속에 놓고, 그 아이디어를 새 연구와 발견으로 이어가 주기를 바란다고 맺는다.

가장 흥미로운 지점

내가 가장 눈여겨본 것은 2,000달러라는 숫자다. 10년 넘게 열려 있던 난제 열 건의 해를 찾는 토큰 비용이 API 요율로 그 정도였다는 대목은, 결과의 난이도와 비용의 비대칭을 그대로 드러낸다. 물론 여기엔 사람이 원고로 다듬는 노동과, 그 논증이 옳은지 가리는 검증의 무게가 빠져 있다. 그래서 OpenAI가 굳이 “모델이 생성하고, 사람이 원고화하고, 다시 모델이 Lean으로 형식화한다"는 세 단계를 나눠 적고, 형식 인증서를 통째로 공개한 점이 눈에 들어온다. 검증 가능성을 결과와 같은 무게로 다루겠다는 신호이기 때문이다. 실제로 저장소의 열두 개 정리는 미완성 표시가 하나도 없고 표준 공리 셋만 쓰며, Comparator라는 독립 검사 도구까지 걸어 뒀다. 다만 논문 PDF와 형식 인증서를 함께 냈다 해도 이것이 동료 심사를 거친 학술 발표는 아니라는 점, 그리고 이 결과들이 공동체의 검토를 어떻게 통과하느냐는 여전히 열린 질문으로 남는다.

출처

OpenAI, “Ten advances in mathematics and theoretical computer science” (2026-07-29) 원문: https://openai.com/index/ten-advances-in-mathematics/ 논문(PDF): https://cdn.openai.com/pdf/ten-proofs-oai.pdf 추론 과정 해설(PDF): https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf Lean 인증서: https://github.com/openai/ten-proofs

원문에 인용할 만한 도식이나 이미지가 없어, 커버는 치비 서소영 삽화로 대신했다.