OpenAI Astra가 푼 10개 수학 난제, 기계 검증은 통과했고 사람 심사는 아직

OpenAI가 2026년 8월 1일 Ten advances in mathematics and theoretical computer science를 공개했습니다. 아직 출시되지 않은 차기 모델 계열 Astra의 내부 버전이 10년 넘게 아무도 주요 결과를 밀지 못한 난제 10개에서 새 증명을 만들었다는 발표입니다.

발표문에 벤치마크 표는 한 장도 없습니다. 대신 OpenAI는 249쪽 논문 PDF, 62쪽짜리 모델 추론 해설, 그리고 Lean 4로 형식화한 증명 저장소 openai/ten-proofs를 Apache-2.0 라이선스로 올렸습니다. 모델이 잘한다는 주장을 점수가 아니라 기계가 검사할 수 있는 파일로 제출한 발표입니다. 저장소는 8월 1일 06시 10분(UTC)에 만들어졌고, 이 글을 쓰는 시점에 스타 327개, 포크 34개가 붙었습니다.

10개 중에 무엇이 큰 결과인가

수학 쪽 결과부터 정리하면 이렇습니다. 각 항목 뒤 괄호는 저장소의 Lean 파일 이름입니다.

• 고차원 구 채우기: Cohn-Elkies 선형계획의 정확한 지수적 감쇠율을 확정했습니다. 논문 표기로 지수는 0.6044...이고, 1978년 Kabatianskii-Levenshtein 값 0.59905576... 이후 일반 구 채우기 지수의 첫 개선입니다. (SpherePacking.lean)
• 이진·구면 부호: 최소거리를 고정했을 때의 고전적 상계를 모든 파라미터에서 지수적으로 개선했습니다. (MetricCodes.lean)
• 비소픽 군: 모든 군이 유한 순열로 근사되는지를 묻던 군론의 오래된 질문에, 근사되지 않는 군을 직접 구성해 답했습니다. (NonSoficGroup.lean)
• Connes 강성 추측 반증: 같은 군 폰노이만 대수를 갖는 서로 동형이 아닌 property-(T) 군을 무한히 많이 만들었습니다. (ConnesRigidity.lean)
• permanent 하계: 나눗셈 없는 회로는 Ω(n² log log n) 게이트, 식은 Ω(n⁴ / log n) 리프가 필요하다는 결과입니다. (Permanent.lean)
• 양자 병렬 반복: 유한한 2인 얽힘 게임 전체에 대해 지수적 병렬 반복 정리를 증명했습니다. (QuantumParallelRepetition.lean)
• 최근접 벡터 문제: 3SAT에서 직접 환원해 n^(1/400) 인수의 근사 난해성을 얻었습니다. 격자 기반 후양자 암호의 난해성 가정과 맞닿는 부분입니다. (GapCVP.lean)
• Ehrhart 부피 추측: 무게중심이 유일한 내부 격자점인 볼록체의 최대 부피가 (n+1)ⁿ / n!임을 모든 차원에서 증명했습니다. (EhrhartVolumeInequality.lean)
• 다색 Ramsey 수: R_k(3) = k^Θ(k)를 주는 초지수 하계로 Erdős 문제 183을 해결했습니다. (MulticolorTriangleRamsey.lean)
• 극단 그래프 이론: Erdős-Simonovits 압축성 추측과 Erdős 퇴화 추측의 반례로 Erdős 문제 146과 180을 정리했습니다. (CompactnessAndDegeneracy.lean)

10개 전부가 같은 무게는 아닙니다. Erdős 문제 목록을 관리하는 Manchester 대학의 Thomas Bloom은 X에서 이번 결과를 "큰 소식"이라고 평하면서, 구성적 결과로는 5월에 나온 단위거리 추측 반례보다 크다는 취지로 말했습니다. Bloom은 과거 OpenAI의 잘못된 수학 주장을 공개적으로 비판한 적이 있는 사람입니다.

2000달러, 일주일, 그리고 공개되지 않은 실패

가장 많이 인용된 숫자는 비용입니다. OpenAI는 발표문에서 "이 문제들의 해답을 찾는 데 필요한 총 토큰은 Sol API 요율로 대략 2000달러어치"라고 적었습니다. Sol은 GPT-5.6이 정식 출시되면서 공개된 계열이고, 지금 누구나 API로 부를 수 있는 모델의 요율입니다.

만들어진 과정은 저장소 formalization.yaml에 기계가 읽을 수 있는 형태로 남아 있습니다. 이 파일이 발표문보다 많은 것을 말합니다.

automation:
  methods:
    - method: "agent"
      models:
        - "Astra (OpenAI)"
      framework: "Codex"
      cost:
        wall_time: "1 week"
review:
  status: "agent-reviewed"

정리하면 OpenAI의 코딩 에이전트 프레임워크인 Codex 위에서 Astra를 일주일 돌린 결과물입니다. 사람이 한 일은 발표문에 따로 적혀 있습니다. 논증은 모델이 생성했고, 사람이 같은 모델과 함께 원고로 정리했으며, 형식화는 다시 모델이 했습니다. 군론 부분에서는 Henry Bradford, Francesco Fournier-Facio 같은 전문가 자문이 있었다고 알려졌지만 이는 자문 기록이지 독립 인증이 아닙니다.

2000달러라는 숫자는 그래서 반쪽입니다. Hacker News 원문 스레드는 449점 319댓글이 붙었고, 가장 많이 공감을 받은 지적은 실험 설계가 공개되지 않았다는 것이었습니다. 사용자 aabhay는 네 가지를 물었습니다. 모델에 총 몇 문제를 줬는지, 그중 몇 퍼센트를 포기했고 그때까지 쓴 비용은 얼마인지, 문제당 시도 횟수는 몇 번인지, 하네스가 잡 클러스터를 썼다면 그 비용은 얼마인지. 성공한 10건의 토큰값만 떼어 공개하면 비용은 얼마든지 작아 보일 수 있습니다.

에이전트 성적이 모델보다 하네스에 좌우된다는 것은 ARC-AGI-3에서 설정 두 개만 바꿔 점수가 뛴 사례에서 이미 확인된 사실입니다. 이번에도 하네스 쪽 정보는 framework: Codex와 wall_time: 1 week 두 줄이 전부입니다.

Lean 커널이 보증하는 것과 보증하지 않는 것

Lean 인증서를 붙였다는 말이 "검증이 끝났다"는 뜻은 아닙니다. 이 구분이 이번 발표를 읽는 데 가장 중요합니다.

기계 검증 쪽은 꽤 단단하게 준비돼 있습니다. 툴체인은 leanprover/lean4:v4.32.0으로 고정돼 있고, 열 개 결과의 Lean 파일 크기는 합쳐서 약 21MB입니다. 가장 큰 GapCVP.lean이 5.3MB, MetricCodes.lean이 4.5MB입니다. ComparatorChallenges/ 폴더에는 결과별 JSON 설정 12개가 들어 있어서, OpenAI가 만든 것이 아닌 외부 커널로 다시 검사할 수 있습니다.

lake exe cache get
lake exe comparator ComparatorChallenges/A_SpherePacking.json

문제는 표 아래쪽 세 줄입니다. Lean 명제가 수학계가 말하는 그 문제를 정확히 옮긴 것인지, 비형식 진술에서 형식 진술로 내려오는 과정이 빠짐없었는지는 커널이 검사하지 않습니다. 저장소의 review.status가 agent-reviewed로 적혀 있는 것도 그래서입니다. 사람 동료심사 기록이 아닙니다. 환경을 부분 재현해 본 kingy.ai는 고정된 환경과 공개 프로젝트 대부분을 다시 만들 수 있었다고 보고하면서도, 이것은 정식으로 부호화된 10개의 연구 주장이지 수학 정전에 등재된 10개의 확정 결과가 아니다라고 정리했습니다.

저자는 누구이고, 모델은 언제 나오는가

OpenAI는 저자 표기를 정면으로 다뤘습니다. 발표문의 해당 대목은 이렇습니다.

AI 시스템이 전적으로 생성한 증명을 두고 사람이 저자라고 주장하는 것은 시스템의 기여와 진짜 사람의 지적 작업 양쪽을 잘못 표현하는 일입니다. 우리는 원고 작성과 Lean 형식화를 도왔고 그 정확성에 책임을 집니다. 다만 수학적 논증 자체는 우리 시스템이 생성했습니다.

이 문장은 6월에 나온 Leiden Declaration on AI and Mathematics를 의식한 것입니다. 국제수학연맹(IMU)이 지지한 이 선언은 AI 기업이 동료심사를 건너뛰고 보도자료로 결과를 내는 관행과 저자 표기 문제를 지적했습니다. OpenAI는 선언 서명자들을 존중한다고 밝히면서도, 결과 공개 방식 자체는 바꾸지 않았습니다. HN에서는 정확성 책임을 지겠다는 약속이 Lean으로 검증된 증명에 대해서는 사실상 부담이 거의 없는 선언이라는 반응도 나왔습니다.

모델 공개 일정은 아직 없습니다. Astra는 The Information이 먼저 보도한 계열로, 여러 에이전트가 몇 시간에서 며칠에 걸쳐 한 문제를 나눠 맡는 구조로 알려졌습니다. 기존 Sol, Terra, Luna와 나란히 놓이며 GPT-6로 낼지 GPT-5 계열 변종으로 낼지도 정해지지 않았습니다. 이름조차 잠정입니다.

공개 전에 관문이 하나 더 있습니다. 6월 2일 서명된 행정명령에 따라 프런티어 모델을 공개 전 최대 30일간 연방 정부가 검토하는 자발적 절차가 8월 1일 확정 기한이었고, Astra가 첫 적용 대상이 될 전망입니다. Sam Altman은 그 직전 워싱턴에서 상원의원과 규제 당국에 Astra를 시연했고, Treasury 장관 Scott Bessent와 Commerce 장관 Howard Lutnick이 회동에 참석했습니다. GPT-5.6 때도 6월 26일부터 7월 9일까지 검증된 20여 개 조직에만 먼저 열었던 전례가 있습니다.

개발자가 지금 당장 쓸 수 있는 것은 모델이 아니라 저장소입니다. Apache-2.0으로 열려 있고, 에이전트가 만든 결과물에 검증 가능한 증거를 붙이는 방식이 어디까지 왔는지 파일 단위로 확인할 수 있습니다. sorry_count: 0까지는 자동화가 도달했고, review: agent-reviewed를 사람 심사로 바꾸는 일은 아직 남아 있습니다.