1. OpenAI가 실제로 공개한 것

OpenAI는 2026년 8월 1일 고차원 기하, 부호이론, 군론, 회로 복잡도, 양자 복잡도, 격자 암호, 볼록기하, 램지이론에 걸친 결과 10건을 발표했다. 수학적 논증은 차기 주요 모델로 소개된 내부 Astra가 만들었고 인간과 같은 모델이 원고와 Lean 인증서를 준비했다고 설명했다.

현재 원고는 253쪽이며 8월 6일 업데이트 표시와 원본 링크가 있다. 따라서 수정 가능한 연구 공개물이지 Astra 공개 버전이나 최종 저널 기록이 아니다. 8월 17일 현재 OpenAI 페이지에는 이 묶음을 승인한 동료평가 학술지가 적혀 있지 않다.

2. 결과 10건이 모두 완전 해결 10건은 아니다

OpenAI도 ‘해결하거나 중대한 진전’이라고 쓴다. 비소픽 군의 구성과 Connes 강직성 추측의 반례가 있는 반면 구 채우기와 부호의 개선된 경계도 있다. 논문은 구 채우기 지수가 1978년 이후 처음 일반적으로 개선됐다고 하지만 경계 개선은 모든 경우의 분류와 다르다.

정확한 표현은 성격이 다른 형식화 기여 10건이다. 각 분야 연구자가 범위·선행성·중요성을 해당 문헌 안에서 판단해야 한다.

  • 해결·구성: 존재를 증명하거나 명시된 질문을 닫는다.
  • 반증: 추측에 대한 반례를 낸다.
  • 경계 개선: 알려진 수치를 전진시키지만 모든 문제를 끝내지는 않는다.
  • 형식 인증: 논리를 확인하지만 중요도를 채점하지 않는다.

3. Lean이 보장하는 범위

All.lean은 결과별 모듈 10개를 import하며 저장소는 Lean 4.32.0, mathlib, Lake를 지정한다. Lean 공식 설명서에 따르면 커널 승인은 파일과 의존성의 정의·정리·공리에서 형식 명제가 따라온다는 뜻이다. 올바른 검증은 미완성 목표와 전술 오류를 잡는다.

OpenAI는 격리 환경과 외부 검사기를 위한 Comparator 과제도 공개했다. 신뢰할 명제를 고정하고 하나의 빌드 경로 의존성을 줄이는 강화 장치다. 그래도 형식 명제가 공동체가 말한 추측과 정확히 같은지라는 의미 문제는 사람이 확인해야 한다.

4. 인증서가 닫지 못하는 네 가지 틈

첫째 번역: 올바른 코드가 비공식 주장보다 약한 명제를 담을 수 있다. 둘째 새로움: 커널은 문헌을 검색하거나 재발견을 감지하지 않는다. 셋째 중요성: 논리적 타당성이 깊이나 유용성을 보장하지 않는다. 넷째 귀속: 인증서는 참고문헌 완전성이나 훈련자료 권리를 증명하지 않는다.

라이덴 선언은 공개, 인간 설명, 적절한 형식 검증을 권하면서도 인간 책임과 동료평가 출판을 유지하라고 요구한다. Lean을 거부하는 것이 아니라 과학적 신뢰 사슬 안에서 위치를 정하는 접근이다.

  • Lean: 인코딩된 도출이 승인됐는가?
  • 분야 심사자: 번역·선행연구·새로움이 맞는가?
  • 학술지: 방법·귀속·중요성이 독립 검토를 통과했는가?
  • 기관: 특권적 모델 접근 없이 재현 가능한가?

5. 2,000달러가 뜻하는 것

OpenAI는 해답을 찾는 데 필요한 총 토큰을 Sol API 가격으로 환산하면 약 2,000달러라고 밝혔다. 이는 토큰 가격 계산이지 프로젝트 원가 공개가 아니다. 실패한 시도, 문제 선정, Astra 훈련 연산, 전문가 시간, 253쪽 원고와 형식화 비용이 모두 포함됐는지 명확하지 않다.

따라서 수학 문제 10건을 2,000달러에 풀었다고 말하면 안 된다. 성공한 발견의 한계 추론비가 연구자 시간보다 매우 낮아질 수 있다는 경제 신호는 크지만, 접근 조건·성공률·인간 검증비가 자동 수학 연구소의 실제 비용을 결정한다.

6. 한국 연구기관의 도입 기준

대학이나 국책연구소는 비공개 평가 문제, 재빌드 가능한 인증서, 분야 전문가 2인의 검토, 실패 실행·토큰·인간 시간 원장을 요구해야 한다. 아이디어 발견비와 이해 가능하고 출판 가능한 증명으로 바꾸는 비용을 분리한다.

초기에는 가설 탐색, 보조정리 제안, 알려진 단계의 Lean 형식화를 맡기고 우선권 발표 전에는 이름이 명시된 인간 승인자를 둔다. 암호·반도체·양자 연구처럼 산업 영향이 큰 분야일수록 검증과 공개 책임을 함께 설계해야 한다.

  • 고정된 도구·의존성으로 인증서를 재빌드한다.
  • 형식 명제와 자연어 주장을 줄마다 대조한다.
  • 홍보 전에 독립 선행성 조사를 한다.
  • 성공 토큰뿐 아니라 실패 실행과 검토비를 공개한다.
  • 정확성·참고문헌·영향의 인간 책임자를 지정한다.