수학 연구의 성과를 후속 논문에서 인용할 때, 필요한 것은 '증명이 존재한다'는 정보만이 아니다. 사용하려는 주장이 어떤 버전으로 작성되었는지, 어떤 전제에 의존하는지, 어느 범위까지 검증되었는지, 그리고 공개 후에 수정된 이력이 있는지를 확인할 필요가 있다. 특히 성과 생성 속도가 빨라질수록, 인용 대상의 정확성과 업데이트 상태를 하나하나 확인하는 작업이 독립적인 공정이 된다.

증명 후보의 생성, 형식 검증(formal verification), 연구상의 평가, 이해, 체계화, 재활용을 나누어 파악하는 생각은 수학적 지식의 성립 조건을 고찰하는 출발점이 된다[1]. 본고에서는 이 중 공개된 성과를 다른 연구의 전제로 계승할 조건에 초점을 맞추고, 실제 수학 원고 리포지토리에서 확인할 수 있는 범위와 거기서 도출되는 관리적 판단을 정리한다.

2026년 10월 6일, OpenAI는 내부 모델이 생성한 수학 연구 성과와 그 일부에 대응하는 Lean 형식 증명을 공개했다[2]. 공개물은 GitHub의 openai/math [3]에 모여 있다. 공개 후인 10월 7일에는 증명상의 문제로 인해 원고가 철회되고 여러 수정 사항이 기록되었다[4]. 이 경과는 공개된 수학적 주장을 참조하는 측에서 무엇이 필요한지를 생각하게 하는 구체적인 예시가 된다.

1. 문제 수, 결과 계열, 원고 수를 개별적으로 식별하기

OpenAI의 공개 리포지토리 openai/math는 약 4,000 문제를 대상으로 모델을 평가했다고 설명하고 있다. 공개 시점에 제시된 규모는 372 결과 계열(result series), 722 원고였으며, 2026년 10월 9일자 README에는 372 결과 계열, 719 원고라고 기재되어 있다[3]. 이 차이를 읽기 위해서는 계산하는 대상을 먼저 구별할 필요가 있다.

이번의 719라는 수치 역시, 722라는 당초의 원고 수가 단순히 수정된 것이 아니라, 10월 7일에 3개 원고가 철회된 후의 게재 규모를 나타낸 것이다. 건수를 읽을 때는 무엇을 계산했는지와 어느 시점의 상태를 계산했는지를 병기할 필요가 있다.

2. Lean의 검증 범위를 원고의 주장에 대응시키기

형식 검증은 특정 형식 명제에 대해, 증명 항이 채택한 형식 체계로 수용되는지 확인하는 것이다. 자연어 논문에 있는 모든 주장을 일괄적으로 보장하는 작업과는 검증 대상의 입자(granularity)가 다르다.

openai/math의 README는 공개물의 검증 단계가 균일하지 않으며, 모든 원고에 Lean 형식화가 첨부되는 것은 아님을 명시하고 있다. 형식화된 결과라 하더라도, 어떤 주장을 대상으로 했는지 확인할 필요가 있다. 이에 대응하는 자산 중 하나가 lean/formalization.yaml이다[5]. 이 파일은 형식화된 주요 결과에 대응하는 원고를 카탈로그화하고 있다.

검증용 정보를 읽기 전에, 공개 리포지토리의 어느 버전을 보고 있는지 고정해야 한다. 아래는 현행 파일 구성을 확인하기 위한 절차이며, 특정 정리에 대한 형식 검증을 실행하는 절차가 아니다.

git clone https://github.com/openai/math.git
cd math
git rev-parse HEAD
...

git rev-parse HEAD가 반환하는 커밋 식별자를 기록해 두면, 나중에 README나 형식화 카탈로그가 업데이트되었을 때도 이번에 확인한 내용의 버전을 특정할 수 있다. lean/README.md에는 검증에 관한 추가 안내가 있다. 형식화 유무를 파일 이름만으로 판단하기보다, 카탈로그와 검증 대상 정리를 대조하는 것이 더 확실하다.

여기서는 적어도 다음 세 가지 대응을 나누어 확인할 필요가 있다.

3. 하나의 증명 오류가 의존하는 원고로 전파된다

2026년 10월 7일자 history.md

은 철회, 증명 수정, 인용 업데이트, 형식화 추가를 개별적으로 기록하고 있다 [4]. 철회와 관련해서는 다음 3개 원고가 언급되었다.

이력에 따르면, 첫 번째 원고의 부호 오류가 특정 소거 논의와 그를 이용하는 두 개의 원고 구성을 무효화했다. 여기서 발생한 것은, 오류를 포함한 원고 1개만의 교체가 아니라, 의존 근원의 주장 변경이 의존 대상 성과의 수용 가능성을 변화시켰다는 사안이다.

설명을 위해 세 가지 원고의 논리적 의존을 다음과 같이 나타낸다. 이는 이력 기술을 간략화한 그림이며, 실제 정리/보조정리의 전체 의존 그래프를 복원한 것은 아니다.

A Weil classes 관련 원고
│
├── B Kuga–Satake 대응 관련 원고
...

같은 날짜의 이력에는 이것과는 별도로 14개 원고의 수정도 있다. 증명 복구, 가정 명확화, 주장 정정 등이 포함된다. 게다가 13개 원고에서는 관련 원고의 개정판을 가리키도록 인용과 버전 날짜가 업데이트되었다.

이들은 변경 의미가 다르다.

여기서 두 종류의 관계를 구분할 수 있다. 하나는 정리 X의 증명이 정리 Y를 전제로 하는 논리적 의존이다. 다른 하나는 원고가 다른 문서나 버전을 참조하는 서지상의 참조이다. 인용의 존재만으로 논리적 의존을 추정하거나, 인용처가 업데이트되었다는 사실만으로 증명의 유효성을 확정하는 것은 적절하지 않다.

4. 버전과 검증 범위와 의존 관계를 동일 단위로 추적한다

공개된 파일들에는 각각 다른 역할이 있다.

README는, 정정과 개정을 새로운 버전으로 기록하고, 이전 버전도 참조 가능한 상태로 유지하는 방침을 보여준다. history.md에 변경의 개요를 집약하고, 원고별 정보로 대상을 특정하는 구조는 성과의 업데이트 상태를 조사할 단서가 된다.

# 이력에 기록된 철회・수정・형식화 항목을 확인한다
grep -nE 'Withdrawals|Fixes|Additional Formalizations' history.md
# 개별 원고의 파일군을 찾는다
...

다만, 공개 리포지토리에서 확인할 수 있는 정보와 재사용할 때 필요한 정보가 같은 형식으로 제공된다는 보장은 없다. 다수의 성과를 지속적으로 참조하는 시스템을 만들려면, 다음과 같은 정보를 하나의 관리 대상으로 대응시키는 설계가 고려될 수 있다.

재활용 판정의 개념적 관리 예시

openai/math 의 기존 스키마가 아님

manuscript:
...

이 예시의 핵심은 status로 원고의 공개 상태를, version으로 개정 상태를 추적하고, claims에 있는 정리 단위의 검증 범위, logical_dependencies에 있는 논리적 의존, bibliographic_references에 있는 서지 참조를 구분하는 것이다. 원고가 수정되었을 때, 대상 정리가 변경된 것인지, 설명만 변경된 것인지를 구별할 수 있다. 형식화(formalization)를 실행한 시점의 커밋 식별자가 기록되어 있다면, 검증한 소스의 버전도 추적할 수 있다.

이 관리 예시는 형식화된 증명이 자연어의 의도에 대응하거나, 미형식화된 증명이 올바르다는 것을 자동으로 보장하는 것은 아니다. 정보를 연결하고 필요한 확인 작업의 대상을 특정하기 위한 구조이다.

5. 후속 연구에 통합하기 전 판단을 공정으로 정의하다

기존의 수학적 성과를 새로운 연구의 전제로 이용할 때, 확인 순서를 고정하면 어느 단계에서 불확실성이 남아 있었는지를 추적하기 쉬워진다.

• 식별한다. 인용하는 결과 계열, 원고, 사용되는 정리, 버전을 특정한다. - 공개 상태를 확인한다. 철회/수정/최신 버전으로의 대체가 있는지 조사한다. - 검증 범위를 확인한다. Lean 형식화가 있는 경우, 이용하는 주장과 가정이 그 대상에 포함되는지 대조한다. - 논리적 의존을 확인한다. 해당 주장이 사용하는 보제나 외부 결과에 효력 상실 또는 조건 변경이 없는지 조사한다. - 수학적인 의미를 평가한다. 원래의 문제와의 일치, 선행 연구, 신규성, 적용 범위를 확인한다.

예를 들어, 어떤 원고의 정리를 사용할 때 최신 버전의 PDF가 참조 가능하고 대응하는 형식화 자산도 존재한다고 가정하자. 그 시점에서 확인할 수 있는 것은 공개된 원고와 검증 자산의 소재이다. 실제로 그 정리를 후속 연구의 전제로 삼기 위해서는, 형식화된 명제의 가정이 사용 상황에 부합하는지 그리고 필요한 의존처의 상태까지 확인하는 것이 요구된다.

이 생각은 AI 생성 수학 고유의 새로운 논리 규칙이 아니다. AI에 의해 성과의 공급량이 증가했을 때, 종래에는 연구자의 독해와 문헌 조사에 내포되어 있던 공정을 추적 가능한 작업으로 분리하는 것이다.

Advisory Group on Mathematics and Artificial Intelligence (AGMAI)는 AI 생성 수학의 책임 있는 공개에 대해 영구적으로 인용할 수 있는 식별자와 개정 이력을 가진 학술 리포지토리 이용, 자연어와 형식 증명을 대응시키는 기계 가독성 정보, 형식화 상태의 명시를 권고하고 있다[7]. 이것들은 성과물을 공개하는 측의 실무인 동시에, 후속 연구자가 검증을 이어받기 위한 정보이기도 하다.

재활용 판단을 단순한 verified: true라는 속성만으로 표현하면, 형식적으로 검증된 주장이 어느 버전의 어떤 정리를 가리키는지, 의존하는 성과가 이후 개정되었는지에 대한 정보가 손실된다. 적어도 **버전(version), 주장(claim), 검증 범위(scope of verification), 의존 관계(dependency), 공개 상태(status)**를 독립적으로 추적할 수 있는 것이 참조 측의 확인 부하를 줄이는 조건이 된다.

6. 재활용 가능한 수학적 지식으로 무엇을 남길 것인가

10월 7일의 철회 사례는, 정확성 확인을 성과물에 한 번만 부여하면 끝나는 관리 방법의 한계를 보여주었다. 증명의 근거가 되는 주장이 개정되면, 그 결과에 의존하는 원고도 재평가의 대상이 된다. 형식적으로 검증된 정리(theorem)조차도, 자연어 주장과의 대응과 그 시점의 검증 범위가 확인 대상으로 남아야 한다.

AGMAI는 2026년 10월 6일 성명에서 OpenAI의 성과 공개를 인간에 의한 이해와 수학적 지식으로 통합이 시작되는 단계로 위치시키고 있다[8]. 여기서의 이해에는 정확성을 읽는 것뿐만 아니라, 어떤 전제가 필요한지, 어떻게 일반화할 수 있는지, 다른 연구에 어떻게 연결할지를 파악하는 작업도 포함된다.

기술적인 귀결은 명확하다. 공개된 수학 원고를 재활용하는 시스템에서는, 원고의 보존과 검색 외에도 **정리의 동일성(identity), 버전(version), 형식 검증 대상(scope of formal verification), 논리적 의존(logical dependency), 철회/수정 이력(retraction/correction history)**을 상호 추적할 수 있도록 할 필요가 있다. 그 정보가 갖춰진다면, 후속 연구자는 공개 시점부터 검증을 다시 해야 하는 범위와 확인 완료로 인계받을 수 있는 범위를 구별할 수 있다.

수학적인 증명이 공동체의 지식으로 작용하는 것은, 옳다고 보고된 시점에만 결정되는 것이 아니다. 다른 연구자가 무엇을 전제로 어떤 상태까지 확인되었는지를 파악하고, 수정 사항을 받으면서 다음 연구에 이용할 수 있을 때, 성과는 지속적으로 재활용 가능한 지식이 된다.

참고문헌

• id774, 증명은 언제 수학적 지식이 되는가 (2026-10-09). https://blog.id774.net/entry/2026/10/09/5760/
• OpenAI, 수학 분야에서 AI의 진척 상황 공유 (2026-10-06). https://openai.com/index/sharing-ai-progress-in-mathematics/
• OpenAI, math. https://github.com/openai/math
• OpenAI, History (역사). https://github.com/openai/math/blob/main/history.md
• OpenAI, formalization.yaml. https://github.com/openai/math/blob/main/lean/formalization.yaml
• id774, Lean으로 AI 생성 증명의 수용 조건과 신뢰 경계를 설계하다 (2026-09-27). https://zenn.dev/id774/articles/4738aa09c9ce43
• 수학 및 인공지능 자문 그룹 (Advisory Group on Mathematics and Artificial Intelligence), AI 생성 수학의 책임 있는 공개 (Responsible Release of AI-Generated Mathematics) (2026-09-29). https://agmai.org/general-sep29/
• 수학 및 인공지능 자문 그룹 (Advisory Group on Mathematics and Artificial Intelligence), OpenAI의 수학적 결과 공개에 관하여 (On OpenAI’s Release of Mathematical Results) (2026-10-06). https://agmai.org/statement-oct6/

논의