OpenAI가 10월 6일 공개한 수학 자료에는 372개 결과 계열로 정리된 원고 722편이 포함되어 있습니다. 한 계열에는 여러 논문이 들어갈 수 있으며, 형식 증명이 다루는 명제는 함께 제공된 원고의 주장보다 좁을 수 있습니다. 논문을 저장소에서 증명 구성까지 따라가면 어떤 주장이 검증 대상으로 선택됐는지 확인할 수 있습니다.
BIG CHANGE는 10월 7일 저장소의 전체 파일 목록과 카탈로그, 일부 증명 산출물을 살펴봤습니다. 이는 문서와 정적 산출물 분석입니다. Lean 라이브러리를 컴파일하거나 증명 검사기를 실행하지 않았으며 수학적 내용을 심사하지도 않았습니다. OpenAI의 발표는 계속 갱신되는 공개 자료를 설명하며 추가 형식화가 이어질 것이라고 밝혔습니다.
달라진 점
- 무엇이 달라졌나: 이제 연구자들은 공동 공개 카탈로그에서 시작해 지원 파일까지, 일부 결과의 경우 형식 명제와 제안된 증명 구현까지 AI가 만든 수백 편의 원고를 추적할 수 있습니다.
- 왜 중요한가: 결과를 활용할지 판단하는 수학자는 실제 검증 대상으로 선택된 명제와 그 가정, 논문과의 관계를 살펴볼 수 있습니다. 저장소의 구성은 범위가 더 좁은 형식 결과가 어디서 끝나고 추가 수학 검토가 어디서 시작되는지 파악하는 데 도움이 됩니다.
- 앞으로 지켜볼 점: OpenAI는 형식화를 추가하고 개정 이력을 보존할 계획입니다. 이 작업을 인용하거나 기반으로 삼는 사람에게는 이런 업데이트가 중요합니다. 검토 기록에는 확인한 버전과 정리가 명시돼야 합니다.
원고 수와 계열 수를 따로 세기
전체 목록에서 preprints/ 바로 아래에 각각 PDF가 들어 있는 원고 디렉터리 722개를 찾았고, reasoning_traces/ 아래에서 PDF 10개를 추가로 확인했습니다. 원고 지도에는 서로 다른 계열 항목 372개와 원고 링크 722개가 있습니다.
이 수치는 서로 다른 대상을 나타냅니다:
산출물 | 독자가 살펴볼 수 있는 내용 |
|---|---|
결과 계열 | 관련 논문을 묶은 단위로, 보조 논증과 결과, 대안적 증명을 포함할 수 있습니다. |
원고 | 고유한 원본 파일과 인용 정보가 있는 개별 수학 문서입니다. |
추론 요약 | 선택된 결과에 관한 모델의 추론을 간략히 정리한 내용입니다. |
Lean 산출물 | 무엇을 확인할지 식별하는 링크와 구성 정보가 포함된 형식적 정의, 명제, 제안된 증명입니다. |
이 저장소의 README는 각 범주를 설명하고 검증 수준이 고르지 않다고 경고합니다. 일부 결과에는 Lean 형식화가 없으며, OpenAI는 형식화되지 않은 작업에 문제가 있을 수 있다고 말합니다. 형식화 카탈로그에는 범위가 ‘Partial progress’로, 검토 상태가 unchecked로 기록돼 있습니다. 이는 게시 메타데이터이며 BIG CHANGE가 검사기를 실행해 얻은 결과가 아닙니다.
공개 파일은 OpenAI 계정 없이 읽을 수 있습니다. 발표에 따르면 생성 모델은 내부용이며 OpenAI는 이를 공개하기 위해 작업 중입니다. 따라서 이 문서에 접근할 수 있다고 해서 해당 모델에도 접근할 수 있는 것은 아닙니다.
증명을 따라가기 전에 버전을 고정하세요
여기서 사용한 저장소 스냅샷은 다음 커밋입니다: adc7f1241b42e322a6451854ab7e4b4c146bf78a, 2026년 10월 6일 21:58:50 UTC에 기록됐습니다. 해당 식별자가 포함된 링크는 살펴본 스냅샷을 가리키고, main가 포함된 링크는 계속 바뀌는 기본 브랜치를 가리킵니다. OpenAI의 README는 수정이나 개정이 나오면 이전 릴리스도 보존하겠다고 설명합니다.
먼저 개요를 살펴보세요. 수학 분야별로 계열을 묶어 보여줍니다. 그런 다음 원고 지도를 이용해 특정 논문을 찾으세요. 논문 디렉터리 이름과 저장소 커밋, 논문에 제공된 인용 정보를 기록해 두세요. 원고 작성일과 공개 컬렉션의 출시일은 다를 수 있습니다.
003 계열에는 7/8보다 오른쪽에 영점이 없는 영역을 주장하는 논문, 11/12보다 오른쪽 영역에 대한 대안 증명, Landau-Siegel 영점에 관한 별도 논문이 있습니다. 첫 번째 논문의 디렉터리에는 9월 30일이라는 날짜와 BibTeX 인용이 있습니다. 어떤 논문인지 기록해 두면 이 주장들을 서로 구분할 수 있습니다.
이 논문의 Lean 범위 페이지는 형식화가 다루는 명제를 설명하고 제외 항목을 밝히며, 논문의 후속 응용은 포함하지 않는다고 말합니다. 제타 결과, Dirichlet 및 Hecke L-함수, 실수 영점의 균일한 간격에 대한 검증 명제를 각각 연결합니다. 선택된 명제 하나를 검사했다고 해서 그 페이지의 모든 항목까지 자동으로 확인되는 것은 아닙니다.
선택한 명제를 구성 파일까지 따라가기
OpenAI의 Comparator 안내서는 003 계열을 예로 듭니다. Comparator는 제안된 Lean 증명을 지정된 과제와 비교하는 도구입니다. 예시 JSON 구성은 하나의 정리를 선택합니다. 논증의 실수부가 7/8을 넘으면 리만 제타 함수가 0이 아니라는 정리입니다.
구성은 과제 모듈과 별도의 해답 모듈을 지정합니다. 표준 공리 propext, Quot.sound 및 Classical.choice, 그리고 enable_nanoda은 false로 설정합니다. Nanoda는 Comparator가 사용할 수 있는 독립 검사기지만, 제공된 구성에서는 활성화되지 않았습니다.
과제 파일에는 sorry가 있습니다. 이는 미완성 증명을 나타내는 Lean의 자리표시자입니다. 여기서는 대조할 명제를 제공하는 역할을 합니다. Comparator 문서는 과제에 이 자리표시자를 허용하지만, 해답에는 올바른 증명이 있어야 한다고 요구합니다. 이 과제에서 sorry 만으로는 별도 해답의 검사 통과 여부를 알 수 없습니다. Comparator 문서.
문서화된 로컬 검사를 하려면 해당 구성과 과제·해답 모듈, 각 모듈의 종속 항목이 필요합니다. 저장소는 Lean 4.34.1을 고정합니다. Lake 매니페스트에는 Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612을 비롯한 종속 항목의 리비전이 기록돼 있습니다.
OpenAI는 comparator, landrun 및 lean4export를 실행 파일 검색 경로에 두도록 요구한 뒤, lean/ 디렉터리에서 실행할 명령을 문서화합니다:
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json이는 게시자가 제공한 지침이며, 우리가 실행한 명령이 아닙니다. 이 지침은 외부 도구 세 가지의 버전을 고정하지 않습니다. 현재 Comparator 문서는 호환되는 lean4export 환경을 요구하고 샌드박스 전제 조건을 설명하며, 실행 성공이 과제와의 일치, 허용된 공리 사용, 커널 승인을 입증하는 조건을 명시합니다. 재현 가능한 보고서라면 설치된 도구 버전과 실제 출력, 저장소 커밋도 기록해야 합니다.
이 Lean 라이브러리 README는 이 대형 라이브러리의 작은 부분만 컴파일하도록 권장합니다. 전체 빌드를 막을 수 있는 Linux 메모리 매핑 제한도 설명합니다. 이 사례에서 로컬 실행 시간이나 하드웨어 비용을 측정하지는 않았습니다.
성공적인 검사를 명시된 범위 안에서 읽기
Lean의 검증 참고 문서는 확인 당시 버전이 4.35.0-rc3이었으며, 형식 증명을 받아들이는 것과 정리의 의미를 해석하는 것을 구분합니다. 이 문서 버전은 저장소가 고정한 도구 버전과 다릅니다.
기본 검사가 성공했다는 것은 커널이 정의, 가져오기, 공리에 따라 형식 명제를 받아들였다는 뜻입니다. 종속 항목에 미완성 증명이 남아 있을 수 있습니다. Lean은 사용된 공리를 확인하는 #print axioms를 문서화하며, 종속성 사슬의 미완성 증명을 나타내는 sorryAx는 종속성 사슬에서 미완성 증명을 나타냅니다.
더 강한 검사는 저장된 증명을 재생하거나 해답을 별도로 지정한 명제와 비교합니다. 그래도 검사 환경과 의도한 의미가 정확히 표현됐는지에 따라 결과가 달라집니다. 따라서 검증 보고서에는 정확한 과제, 허용된 공리, 외부 검사기 설정을 기록해야 합니다. 커널의 승인이나 과제와의 일치만으로 학술지 게재가 승인됐거나 원고의 모든 주장이 형식화됐다고 볼 수는 없습니다.
컴퓨팅 수치는 생성에 관한 것입니다
OpenAI에 따르면 결과 하나당 평균 컴퓨팅 작업량은 ChatGPT Pro가 약 세 시간 동안 사고한 것과 맞먹습니다. README에는 평가에서 약 4,000개 문제를 제시한 뒤 결과를 묶고 중요도에 따라 선별했다고 적혀 있습니다. 통상 절차의 예외도 밝힙니다. 이는 회사가 공개한 생성 관련 수치이며, 독자의 Lean 검사 비용이나 총 달러 지출을 뜻하지 않습니다. 출시 발표, 생성 과정 설명.
003 계열을 살펴보면 특정 제타 명제와 제안된 해답, 검사기가 허용한 공리를 확인할 수 있습니다. 제공된 예시에서 Nanoda가 비활성화된 점도 확인됩니다. 해당 구성의 검사가 성공하는지는 실제로 실행하고 기록해야 알 수 있습니다.
출처 및 더 읽을거리
- 10월 6일 OpenAI 발표는 출시일과 모델의 내부용 상태, 추가 계획, 컴퓨팅 추정치를 확인해 줍니다. 이는 개발사가 자체 작업을 설명한 자료입니다.
- 고정된 저장소에는 여기서 살펴본 카탈로그와 원고 파일, 증명 구성이 들어 있습니다. 수치는 전체 파일 목록과 원고 지도에서 산출했으며, 일부 형식 파일은 실행하지 않고 읽었습니다. 개요의 구성 방식을 확인하려고 LaTeX 원본도 살펴봤습니다.
- Lean 검증 참고 문서는 증명 검사의 의미와 한계를 설명합니다. 참고한 문서 버전은 4.35.0-rc3이고, OpenAI 프로젝트는 Lean 4.34.1을 고정합니다.
- Comparator 문서는 과제·해답 파일, 환경 요건, 조건부 보장을 설명합니다. 이 컬렉션의 검증 결과를 보고하지는 않습니다.
- Curtis Pyke의 Kingy.ai 리뷰는 해당 공개 자료를 독립적으로 정적 분석합니다. 독립적인 Lean 실행은 없었다고 명시하므로 증명 검사를 재현한 자료로 보지 않습니다.
- BIG CHANGE의 이전 AI 수학 보고서는 5월부터 9월까지의 흐름을 다룹니다. 이 기사는 새 컬렉션의 산출물 구조와 점검 과정을 살펴봅니다.
