OpenAI 수학 원고 719개를 읽는 법: 철회와 형식 검증의 범위

OpenAI가 공개한 수학 원고를 읽을 때는 무엇을 주장하는지와 어디까지 검증했는지를 함께 확인해야 한다. 원고 수, 관련 결과를 묶은 결과군, 형식화된 주요 결과 수는 서로 다른 집계다. 철회나 수정도 오류가 생긴 지점과 다른 원고에 미친 영향을 나눠 봐야 한다.

이 글은 2026년 10월 12일에 확인한 공식 저장소와 Lean 문서 기준 해설이다. 개별 증명을 재현하거나 전체 원고의 학술적 정당성을 심사한 결과는 아니다. 같은 날의 다른 소식은 10월 12일 AI·코딩·테크 브리핑에서 확인할 수 있다.

719개 원고와 372개 결과군은 무엇이 다른가

현재 README는 원고 719개를 결과군 372개로 묶는다. 결과군 하나에 주된 결과와 동반 논증, 파생 결과, 대안 증명 등이 들어갈 수 있으므로 두 숫자를 독립적인 난제 해결 건수로 읽어서는 안 된다.

커밋 목록이 10월 6일로 표시하는 초기판 README에는 722개 원고·372개 결과군이 적혀 있다. 지금의 수치를 인용할 때는 확인일을 붙이고, 최초 공개 규모를 설명할 때는 해당 고정판을 연결하는 편이 정확하다.

철회 3개와 수정 14개, 참조 갱신 13개를 나눠 읽는다

10월 7일자 변경 이력은 한 원고의 부호 오류가 핵심 구성을 무효로 만들었고, 그 구성에 의존한 다른 두 원고까지 철회했다고 설명한다. 여기서 살펴볼 것은 철회 건수뿐 아니라 원고 사이의 의존성이다.

이력의 구분	기록된 범위	독자가 확인할 질문
철회 3개	부호 오류가 있는 원고와 그 결과에 의존한 원고 2개	내가 읽는 결과가 철회된 구성에 기대고 있는가?
별도 수정 14개	증명 수선, 명제·가정·의존성 명확화, 낡은 인용 정정	이전 판과 현재 판에서 주장이나 적용 조건이 달라졌는가?
추가 참조 갱신 13개	개정된 동반 원고의 참조와 판본 날짜 갱신	연결된 증명이 어느 판본을 가리키는가?

세 항목을 모두 같은 종류의 증명 오류로 합산하면 변경 이력의 의미를 잃는다. 특히 인용 판본 갱신과 주된 논증의 수선은 독자가 다시 읽어야 할 범위가 다르다.

300/719라는 형식화 비율의 범위

같은 변경 이력이 제시하는 집계는 **주요 결과(top-line results) 300개, 원고 719개를 분모로 약 42%**다. 372개 결과군을 분모로 계산한 비율도, 독립 학술 심사를 마친 원고 비율도 아니다. 이력은 형식화 6개 추가와 보조 결과 관련 추가 5개도 구분한다.

형식화 파일이 있다는 사실만 보고 논문 전체를 검증했다고 해석하는 것도 조심해야 한다. 저장소의 Comparator 안내는 보조 결과용 비교가 해당 논문의 주정리를 검증하는 것은 아니라고 명시한다. 따라서 어떤 정리가 검사 대상인지 먼저 확인해야 한다.

테스트·형식 검증·독립 검토는 어떤 질문에 답하는가

Lean 공식 입문은 형식 검증을 정확한 수학적 표현으로 적은 주장에 논리·계산 방법을 적용하는 일로 설명한다. 증명은 정의와 공리, 앞서 증명한 결과에 기대므로, 검사 대상 명제와 전제를 읽는 일이 함께 필요하다.

아래는 증거를 읽기 위한 비교다. 이번 저장소가 세 과정을 모두 마쳤다는 뜻은 아니다.

확인 방식	주로 답하는 질문	추가로 살펴볼 부분
구현 테스트	준비한 입력과 실행 조건에서 기대한 동작이 나왔는가?	빠뜨린 입력·실패 조건, 운영 환경과의 차이
형식 검증	명시한 정의·가정 아래에서 검사 대상 명제의 증명이 성립하는가?	원고의 주장과 형식화된 명제의 대응, 주정리인지 보조정리인지
독립 학술 검토	논문의 논증·적용 조건·기존 연구와의 관계를 다른 연구자가 어떻게 평가하는가?	검토 대상 판본, 검토 범위와 공개된 지적 사항

형식화는 사람이 모든 추론 단계를 눈으로만 확인해야 하는 부담을 줄일 수 있다. 다만 무엇을 형식화했는지와 그것이 원래 문제를 충실하게 표현하는지는 여전히 독자가 확인할 질문이다. 특정 검사 결과를 논문 전체의 새로움이나 활용 가치로 곧바로 확장할 수는 없다.

원고를 읽을 때의 확인 순서

다음 순서는 이 글에서 제안하는 독해 절차다. 개별 원고를 활용하거나 다른 사람에게 소개할 때 확인 범위를 남기는 데 목적이 있다.

원고와 판본을 고정한다. 제목·파일 경로·날짜 또는 커밋을 기록한다. 현재 카탈로그의 숫자를 과거 공개 규모와 섞지 않는다.
변경 이력을 먼저 읽는다. 철회·실질 수정·참조 갱신 중 해당하는 것이 있는지 확인하고, 의존한 동반 원고도 따라간다.
형식화 대상을 대조한다. 형식화 카탈로그에서 원고와 증명 파일을 찾고, 주정리와 보조 결과의 범위를 구분한다.
검사 조건과 수행 여부를 기록한다. Lean 안내와 Comparator 설정을 확인한다. 직접 실행했다면 환경·명령·결과를, 실행하지 않았다면 문서 확인 범위를 남긴다.
독립 검토의 근거를 별도로 확인한다. 특정 연구자의 검토가 있다면 대상 판본과 지적 내용을 원문에서 읽는다. 저장소에 실렸다는 사실만으로 이 단계를 대신하지 않는다.

이 관점은 AI가 만든 코드를 검토할 때도 도움이 된다. 테스트 통과와 권한·운영 검증이 각각 무엇을 확인하는지 나누는 방법은 AI 코드 생성 이후의 백엔드 검증에서 이어서 다룬다. 수학 증명과 서비스 구현의 검증을 동일시하기보다, 증거가 뒷받침하는 주장 범위를 기록하는 습관을 가져올 수 있다.

참고 자료

OpenAI math README — OpenAI, 확인일 2026-10-12
OpenAI math 초기판 README — OpenAI, 초기 커밋 2026-10-06
OpenAI math 커밋 목록 — OpenAI, 확인일 2026-10-12
OpenAI math 변경 이력 — OpenAI, 2026-10-07자 이력, 확인일 2026-10-12
Comparator checking instructions — OpenAI, 확인일 2026-10-12
Formalization catalogue — OpenAI, 확인일 2026-10-12
Lean library 안내 — OpenAI, 확인일 2026-10-12
Theorem Proving in Lean 4: Introduction — Lean, 확인일 2026-10-12