안녕하세요, 미니지식공간입니다.
OpenAI Astra가 만든 수학·이론전산 결과 10건의 Lean 4 증명이 2026년 8월 1일 openai/ten-proofs 저장소로 공개됐다. 발표 자료를 읽는 것보다, Lean 4(논증을 형식화해 기계가 검사하게 하는 증명 보조 도구) 인증서를 로컬에서 직접 빌드해 보는 쪽이 이 발표의 성격을 더 정확히 알려준다. 이 글은 저장소 구조, 빌드 절차, 그리고 그 빌드가 실제로 보장하는 범위를 정리한다.
저장소가 담고 있는 것
OpenAI 공식 발표(2026년 8월 1일)에 따르면 결과는 차기 주요 모델 Astra의 미공개 내부 버전이 생성했고, 사람이 같은 모델로 원고를 준비한 뒤 모델이 각 논증을 Lean으로 형식화했다. 저장소는 Apache-2.0이며, 결과 하나당 Lean 파일 하나가 대응한다. 249쪽 원고와 추론 과정 기록 PDF도 함께 공개됐다.
| # | 결과 | Lean 모듈 |
|---|---|---|
| 1 | 구 채우기 밀도 상한, Cohn–Elkies 임계값 도달 | SpherePacking |
| 2 | 이진·구면 부호 상한 지수적 개선 | MetricCodes |
| 3 | 비소픽(non-sofic) 군 구성 | NonSoficGroup |
| 4 | 콘(Connes) 강성 추측 반례 | ConnesRigidity |
| 5 | 퍼머넌트 산술 공식 하한 n⁴/log n | Permanent |
| 6 | 2인 양자 게임의 지수적 병렬 반복 | QuantumParallelRepetition |
| 7 | CVP 다항 인자 근사 난해성 | GapCVP |
| 8 | 에르하트(Ehrhart) 부피 추측 | EhrhartVolumeInequality |
| 9 | 다색 삼각형 램지 수 하한(에르되시 183) | MulticolorTriangleRamsey |
| 10 | 극단 그래프 콤팩트성·퇴화 추측 반례(에르되시 146, 180) | CompactnessAndDegeneracy |
로컬 빌드 절차
README가 명시한 툴체인은 Lean 4.32.0, mathlib, Lake다. elan(Lean 툴체인 관리자)이 설치돼 있으면 mathlib 캐시를 내려받고 열 개 형식화를 한 번에 빌드할 수 있다. 아래 명령은 저장소 README에 그대로 실려 있는 것이다.
# 출처: https://github.com/openai/ten-proofs (README)
git clone https://github.com/openai/ten-proofs.git
cd ten-proofs
# mathlib 캐시 내려받기
lake exe cache get
# 열 개 형식화 전체 빌드
lake build All개별 결과만 확인하려면 모듈 이름을 Lake에 넘기면 된다.
lake build SpherePacking툴체인 버전은 저장소의 lean-toolchain에 고정돼 있고, 의존성은 lake-manifest.json과 lakefile.toml이 관리한다. 여기서 lake exe cache get을 건너뛰면 mathlib을 처음부터 컴파일하게 되므로 시간이 크게 늘어난다. 저장소에는 ComparatorChallenges 디렉터리도 있는데, README는 이를 Comparator를 이용한 독립 증명 검사 안내로 소개한다.
빌드가 보장하는 범위
lake build All이 성공했다면, Lean 커널이 각 파일의 형식 진술이 정의와 추론 규칙으로부터 도출된다고 확인했다는 뜻이다. 이 절차는 산문 증명이 감출 수 있는 누락 단계나 잘못된 연역을 잡아낸다. 다만 형식 진술이 원래의 수학 문제를 옳게 옮겼는지는 사람이 원고와 대조해야 하고, 결과의 중요도 평가와 저널 동료 심사는 또 다른 절차다.
Astra 자체는 비공개다. 인증서를 빌드해도 모델에 접근하거나, 이번 공개 범위 밖의 문제에서 모델이 어떻게 동작하는지는 알 수 없다. 즉 이 저장소는 "결과의 검증 가능성"을 열어 주지만 "생성 과정의 재현성"까지 열어 주지는 않는다.
비용 숫자를 어떻게 읽을까
OpenAI는 열 개 해를 찾는 데 필요한 토큰 비용을 Sol API 요금 기준 약 2,000달러로 추정했다(OpenAI 자체 추정, 2026년 8월 1일). 이 값은 특정 시점의 가격표에 종속된다. API 단가 변동이 이런 추정치를 어떻게 흔드는지는 앞서 정리한 GPT-5.6 Luna 가격 인하 글의 계산 방식과 함께 보면 감이 잡힌다.
또한 이 추정에는 실패한 탐색 시도, 연구 인력의 시간, 형식화 과정에서 든 추가 토큰이 포함되는지 명시되지 않았다. 벤치마크 비용처럼 단일 실행 단가로 인용하기에는 전제가 부족하다.
남은 논쟁
2026년 6월 국제수학연맹(IMU)이 지지한 라이덴 선언(Leiden Declaration)은 AI 기업들이 동료 심사를 우회해 결과를 발표하는 관행을 문제 삼았다고 The Next Web이 2026년 8월 1일 보도했다. 같은 기사는 OpenAI 수학 연구 책임자 세바스티앙 뷔벡(Sebastien Bubeck)이 X에서 결과를 확인하며 "beautiful"이라고 표현했다고 전했다.
Implicator.ai는 2026년 8월 1일 기사에서 이번 발표에 특정 증명을 부정한 외부 수학자의 실명 반론이 포함되지 않았다고 짚었고, 맨체스터대 토머스 블룸(Thomas Bloom)이 X에서 "big news"라고 평가했다는 The Decoder 보도를 인용했다. 같은 보도에서 OpenAI 연구원 노엄 브라운(Noam Brown)은 "아직 밀레니엄 문제는 없다"며 범위를 한정했다.
자주 묻는 질문
Q. OpenAI Astra API는 언제 열리나?
2026년 8월 1일 발표 기준으로 공개 일정은 공지되지 않았다. OpenAI는 Astra를 "차기 주요 모델"이라고만 표현했고, 이번 결과도 미공개 내부 버전에서 나왔다고 밝혔다.
Q. Lean 4가 없어도 증명을 확인할 수 있나?
직접 검사하려면 Lean 4.32.0 툴체인이 필요하다. 다만 249쪽 원고와 추론 과정 기록 PDF가 공개돼 있어, 논증 흐름 자체는 컴파일러 없이도 읽을 수 있다.
Q. mathlib 캐시 없이 빌드하면 어떻게 되나?
lake exe cache get을 생략하면 mathlib을 소스에서 전부 컴파일한다. README가 캐시 명령을 먼저 안내하는 이유이며, 빌드 시간을 줄이려면 이 단계를 건너뛰지 않는 편이 좋다.
마무리
이번 공개의 실질적 의미는 결과 자체보다 검증 형식에 있다. 모델은 닫혀 있고 인증서는 열려 있는 구조가, AI가 만든 연구 산출물을 다루는 기본형이 될지 지켜볼 만하다.
출처
- OpenAI, "Ten advances in mathematics and theoretical computer science", 2026년 8월 1일 — https://openai.com/index/ten-advances-in-mathematics/
- openai/ten-proofs (Apache-2.0) — https://github.com/openai/ten-proofs
- The Next Web, 2026년 8월 1일 — https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups
- Implicator.ai, 2026년 8월 1일 — https://www.implicator.ai/openai-astra-10-math-problems-lean-proofs/
본 글은 공개 자료를 바탕으로 정리했으며, 세부 내용·수치는 원 출처·공식 문서와 대조 확인을 권장합니다.
