내부 모델이 구 패킹·군론·연산자 대수 등에서 결과 제시, Lean 증명과 함께 공개
2026년 8월 1일 OpenAI는 차기 주요 모델 패밀리로 지칭되는 내부 버전 Astra가 수학과 이론 컴퓨터 과학 분야에서 최소 10년 이상 진전이 없었던 10개 문제에 대한 새로운 결과를 냈다고 발표했다. 결과는 249쪽 분량의 원고, 각 결과에 대한 모델의 사고 과정 서술, 그리고 Lean 4로 작성된 기계 검증 가능 증명 파일과 함께 공개됐다. 전체 토큰 비용은 Sol API 기준으로 약 2,000달러 수준으로 추산된다.
이 발표는 AI가 벤치마크를 넘어 실제 연구 수준의 기여를 할 수 있는지에 대한 논의를 다시 한번 촉발했다. 동시에 수학 커뮤니티가 최근 강조해 온 검증·귀속·접근성 문제를 정면으로 마주하게 만들었다.
발표된 10개 결과의 범위와 내용
OpenAI가 제시한 결과는 고차원 기하, 코딩 이론, 군론, 연산자 대수, 회로 복잡도, 양자 복잡도, 격자 암호, 극단 조합론 등 여러 분야에 걸쳐 있다. GitHub에 공개된 Lean 저장소와 공식 설명에 따르면 주요 내용은 다음과 같다.
- 고차원 구 패킹: Cohn–Elkies 선형 계획법 프레임워크를 통해 점근적 상한을 개선해 해당 방법의 한계에 도달. 1978년 이후 일반적인 상한에 대한 첫 의미 있는 진전으로 평가된다.
- 이진·구면 부호: 최소 거리에 따른 이진 부호의 최대 크기에 대한 지수적으로 더 강한 상한, 그리고 구면 부호에 대한 대응 결과.
- 비소픽 군(non-sofic groups): 유한 순열 근사가 불가능한 군의 명시적 구성. Gromov가 1999년 소픽성 개념을 도입한 이후, Weiss가 2000년경 제기한 “모든 가산 군이 소픽인가”라는 질문에 부정적인 답을 제시한 것으로 보인다.
- Connes 강성 추측: 특정 군이 그 군의 폰 노이만 대수에 의해 유일하게 결정된다는 추측에 대한 반례 구성.
- 산술 회로 복잡도: 영구식(permanent) 계산에 대한 새로운 하한, 특히 공식(formula)에 대해 수준의 하한.
- 양자 병렬 반복: 일반적인 2인 양자 게임에 대한 지수적 병렬 반복 정리.
- 최근접 벡터 문제(CVP): 근사 경도에 대한 다항 인자 하한. 격자 기반 후양자 암호와 직접 연결된다.
- Ehrhart 부피 추측: 중심이 유일한 내부 격자점인 볼록 체의 최대 부피를 모든 차원에서 결정.
- 다색 램지 수: 다색 삼각형 램지 수에 대한 초지수적 하한으로 Erdős 문제 183 해결.
- 극단 그래프 이론: 컴팩트니스와 퇴화성 추측에 대한 반례로 Erdős 문제 146·180 해결.
이 중 비소픽 군 구성과 구 패킹 상한 개선, Connes 강성 반례가 특히 주목받고 있다. 비소픽 군은 기하군론에서 수십 년간 존재 여부 자체가 열려 있던 문제였고, 구 패킹은 고전적인 기하학적 최적화 문제의 점근적 한계를 다루는 주제다.
검증 방식: Lean 증명의 역할과 한계
OpenAI는 모델이 생성한 논증을 인간이 원고 형태로 정리한 뒤, 다시 모델이 Lean 4로 형식화하는 과정을 거쳤다고 밝혔다. 공개된 저장소는 Lean 4.32.0과 Mathlib에 고정되어 있으며, 누구나 lake build 명령으로 검증할 수 있다. 이는 “AI가 할루시네이션을 냈을 가능성”을 크게 줄이는 장치다. 형식 증명이 통과하면 적어도 정의된 공리 체계 안에서 논리적 오류는 없다.
그러나 Lean 검증과 수학적 채택은 다르다. 형식 증명은 다음과 같은 지점을 보장하지 않는다.
- 형식화된 정의가 해당 분야의 전통적인 문제 진술과 정확히 일치하는지
- 원고의 비형식적 요약과 실제 Lean 정리 사이의 대응이 완전한지
- 결과의 신규성과 역사적 맥락이 정확한지
실제로 발표 직후 일부 결과(특히 Connes 강성 관련)에 대해 형식적 진술이 전통적인 추측의 가설(ICC 조건 등)을 충족하는지에 대한 초기 질문이 제기되고 있다. 이는 독립적인 전문가 검토가 여전히 필수적임을 보여준다. 현재 시점에서 확인할 수 있는 것은 “10개의 진지하고 형식적으로 인코딩된 연구 주장”이 공개됐다는 사실까지다.
비용과 방법론의 시사점
전체 탐색에 약 2,000달러 수준의 토큰 비용이 들었다는 점은 주목할 만하다. 이는 테스트 타임 컴퓨트(test-time compute)를 연구 문제에 적용했을 때의 효율성을 시사한다. OpenAI 측은 이전에도 일부 미해결 문제에 도전했으나 실패했다고 밝혔으며, 밀레니엄 문제는 아직 손대지 못했다고 언급했다.
방법론적으로는 “모델이 핵심 논증을 생성 → 인간이 모델과 함께 원고 정리 → 모델이 Lean으로 형식화”라는 하이브리드 형태다. OpenAI는 귀속을 명확히 했다. “완전히 AI가 생성한 증명을 인간 저작으로 주장하는 것은 시스템의 기여와 인간 지적 노동의 본질을 모두 왜곡한다”는 입장을 밝히고, 원고 준비와 형식화에 대한 책임은 자신들이 지되 수학적 논증 자체는 시스템에 돌렸다. 이는 최근 수학계의 우려를 의식한 표현으로 읽힌다.
수학 커뮤니티의 반응과 구조적 긴장
발표 직후 일부 연구자는 긍정적인 반응을 보였다. Erdős 문제 사이트를 운영하는 Thomas Bloom은 “큰 뉴스”라며, 특히 구성(construction) 측면에서 이전의 단위 거리 추측 반례보다 더 중요할 수 있다고 평가했다. 구 패킹과 비소픽 군 결과가 그 중심에 있다.
동시에 더 넓은 맥락이 존재한다. 2026년 6월 발표된 Leiden Declaration on Artificial Intelligence and Mathematics는 AI가 수학 연구에 미치는 영향에 대한 수학자들의 공동 입장을 정리한 문서다. 국제수학연맹(IMU)의 지지를 받았으며, 주요 우려는 다음과 같다.
- 검증 가능성: 독점 모델이 생성한 결과를 어떻게 독립적으로 확인할 것인가
- 귀속과 신용: AI 기여를 어떻게 정직하게 표시할 것인가
- 접근성 불평등: 최신 모델에 접근할 수 있는 연구자와 그렇지 못한 연구자 사이의 격차
- 연구 우선순위 왜곡: AI가 잘 다루는 문제 유형으로 관심이 쏠릴 가능성
OpenAI의 이번 발표는 Lean 공개와 귀속 명확화라는 점에서 이전보다 진전된 형태를 취했다. 그러나 모델 자체는 여전히 비공개이며, 훈련 데이터와 탐색 과정의 세부 사항도 외부에서 재현하기 어렵다. 이는 Leiden 선언이 지적한 구조적 긴장을 완전히 해소하지는 못한다.
더 넓은 의미와 남은 질문
이 사건은 세 가지 축에서 의미가 있다.
첫째, 과학적 추론 능력의 실증. 벤치마크 점수가 아닌 실제 열린 문제에 대한 결과물이 형식 증명과 함께 나왔다는 점은 AI 연구 커뮤니티에 강한 신호를 보낸다. 동시에 “성공한 10개”만 공개되고 실패한 시도의 규모는 불투명하다는 점도 함께 고려해야 한다.
둘째, 수학 연구 프로세스의 변화. Lean과 같은 형식 검증 도구가 AI 결과물을 받아들이는 데 필수적인 필터로 자리 잡을 가능성이 커졌다. 이는 장기적으로 수학의 검증 문화를 강화할 수도 있고, 형식화 비용이 높은 분야를 상대적으로 불리하게 만들 수도 있다.
셋째, 인프라와 거버넌스. 저비용으로 연구 수준의 결과가 나올 수 있다는 점은 테스트 타임 컴퓨트의 잠재력을 보여준다. 그러나 그 능력이 소수의 조직에 집중될 경우, 수학이라는 학문의 공공성과 접근성 문제가 더욱 부각될 수밖에 없다.
현재 시점에서 가장 중요한 다음 단계는 독립적인 전문가 검토다. Lean 파일이 통과했다는 사실과, 그 파일이 해당 분야의 표준 문제 진술을 정확히 포착했는지, 그리고 결과가 실제로 새로운 기여인지 여부는 별개의 문제다. 수학 커뮤니티가 이 10개 결과를 어떻게 소화하고, 수정하고, 확장할지가 앞으로 수개월간 지켜볼 핵심이 될 것이다.
OpenAI가 제시한 자료는 이례적으로 검사 가능성이 높다. 그 점이 이번 발표를 단순한 홍보성 주장과 구분 짓는 가장 중요한 요소다. 이제 그 검사의 결과가 나와야 한다.