[기획] AI가 722편의 수학 원고를 한꺼번에 내놓자 3편이 사라졌다—OpenAI ‘증명 홍수’와 인간 검증의 병목

도서관 문 앞에 수학책 722권이 하루아침에 쌓였다고 생각해 보자. 하루에 한 권씩 읽어도 주말 없이 거의 2년이 걸린다. 그런데 이 책들은 눈으로 읽기만 하면 되는 교양서가 아니라, 한 줄씩 논리를 확인하고 기존 연구와 대조해야 하는 수학 원고다. OpenAI가 2026년 10월 6일 미공개 내부 프런티어 모델이 만든 원고 722편을 공개하면서 수학계는 바로 이런 장면을 마주했다. 그러나 공개 직후 핵심 원고 한 편에서 부호 오류가 발견됐고, 그 구성을 이용한 다른 두 편까지 모두 철회됐다.

제목처럼 세 편이 흔적 없이 ‘사라진’ 것은 아니다. 철회 공지와 오류 설명이 붙었고, 철회 전 PDF로 이어지는 저장소 리비전도 보존됐다. 개별 원고 공지는 10월 6일 철회라고 적었으며, 저장소 변경 이력에는 세 편의 철회가 10월 7일자 갱신으로 기록됐다. 철회는 해당 증명이 주장을 확립하지 못했다는 뜻이지, 세 원고가 다룬 수학 명제 자체가 거짓으로 판명됐다는 뜻은 아니다.

722개의 독립 발견이 아니라 372개의 결과 묶음

숫자를 먼저 구분해야 한다. 최초 공개된 722편은 서로 독립된 난제 722개를 해결한 목록이 아니다. 주된 결과와 보조 논증, 귀결, 대안 증명처럼 서로 관련된 원고를 묶은 372개 결과군이다. 한 사건을 두고 본보도와 해설, 후속보도가 함께 나오는 것과 비슷하다. 3편이 철회된 뒤 2026년 10월 15일 확인된 현행 목록은 원고 719편과 결과군 372개다.

OpenAI는 기존 수학 평가에서 성능이 포화된 뒤 공개 연구 문제로 평가 범위를 넓혔다고 밝혔다. 모델에는 약 4,000개 문제가 제시됐고, 출력물을 결과군과 원고로 정리한 뒤 일정 수준의 중요성을 요구해 공개 목록을 만들었다. 하지만 문제와 결과군, 원고가 일대일로 대응하지 않기 때문에 722를 약 4,000으로 나눠 성공률을 계산할 수는 없다. 공개되지 않은 문제를 모두 실패로 간주할 수도 없다.

대다수 결과는 같은 절차와 미공개 내부 모델로 생성됐지만 예외도 있었다. 리만 제타함수의 영점 없는 영역과 CM 아벨 다양체의 호지 추측에 관한 연구는 다른 경우였고, ‘Re(s)>11/12’ 영점 없는 영역 원고는 사람이 가독성을 위해 편집했다. 모든 원고가 하나의 동일한 프롬프트로 완전 자동 생성됐다고 표현할 수 없는 이유다. 공개된 모델 추론 자료도 전체 원 기록이 아니라 10개 결과군에 대한 축약 요약이다.

OpenAI가 밝힌 평균 계산량은 결과 하나당 ChatGPT Pro thinking 약 3시간 상당이다. 이는 실제로 시계로 잰 작성 시간이나 GPU 사용시간, 비용을 뜻하지 않는다. 여기서 ‘결과’가 원고 한 편인지 결과군인지도 저장소 설명만으로 명확하지 않다. 따라서 이 수치에 372나 722를 곱해 전체 계산시간과 개발기간을 추정하는 것은 근거가 없다.

‘+1’이 ‘-1’로 바뀌자 세 원고가 흔들렸다

철회의 출발점은 ‘Algebraicity of Weil classes on split abelian eightfolds’라는 원고였다. 이 원고는 역 안정화 궤적의 부호를 각각 ‘+1’로 계산해 교차점 계수가 0이 된다고 주장했다. 하지만 반대 방향성을 반영한 실제 부호는 각각 ‘-1’이었고, 계수는 0이 아니라 ‘-2m’이 됐다. 그 결과 Eliashberg–Murphy 소거 정리를 적용하는 데 필요한 전제가 무너졌다.

문제는 이 원고 하나에서 멈추지 않았다. ‘Algebraicity of Kuga–Satake Correspondences for K3 Surfaces’와 ‘The rational Hodge conjecture for products of K3 surfaces’가 첫 원고의 구성을 사용하고 있었기 때문이다. 건물 1층의 기둥 계산이 틀리자 그 위에 올린 층도 함께 사용할 수 없게 된 셈이다. 소프트웨어로 비유하면 공용 라이브러리의 오류가 이를 불러 쓰는 여러 프로그램에 동시에 영향을 준 장면과 닮았다.

이 사례는 대량의 AI 원고를 독립된 파일 더미가 아니라 의존관계로 얽힌 결과망으로 봐야 한다는 점을 보여준다. 그렇다고 3편을 722편으로 나눈 값을 전체 오류율로 해석해서도 안 된다. 현재 철회된 수를 계산한 값일 뿐, 나머지 원고의 정확도를 증명하는 통계가 아니기 때문이다. 2026년 10월 15일 현재 719편 전체에 대한 독립적인 전수 재현이나 동료심사가 끝났다는 근거는 확인되지 않았다.

같은 저장소 갱신에서는 별도의 14편도 증명 보수, 명제 수정, 가정과 의존관계 명료화, 오래된 인용 정정 등을 위해 개정됐다. 이어 13편은 수정된 동반 원고를 인용하도록 참고문헌과 버전 날짜가 갱신됐다. 수정 사유와 심각도가 서로 달라 이 숫자를 오류율로 묶을 수는 없지만, 문제가 발견된 원고가 철회된 세 편뿐이라고 단정할 수도 없다.

Lean이 확인하는 것과 확인하지 못하는 것

대량 생산된 증명을 검사할 수단으로 거론되는 것이 Lean이다. Lean은 형식 명제와 증명 항을 작은 커널로 검사하는 정리증명기다. 사람이 쓴 자연어 문장을 컴퓨터가 다룰 수 있는 엄밀한 기호로 옮긴 뒤, 주어진 형식 체계 안에서 결론이 논리적으로 도출되는지를 확인한다.

저장소는 최상위 결과 형식화 비율을 ‘300/719’, 약 42%로 표시했다. 좌석 10개 중 약 4개에 최상위 결과를 대상으로 한 형식화 자료가 붙은 셈이다. 이를 원고 300편의 모든 문장과 귀결이 완전히 검증됐다고 바꿔 말해서는 안 된다. 나머지 약 58%가 틀렸다는 뜻도 아니다. 같은 갱신에는 최상위 결과 형식화 6개와 보조 결과를 다룬 기타 추가분 5개도 기록됐다.

Lean의 검사는 강력하지만 범위가 정해져 있다. 바코드 검사기가 등록된 정보와 코드가 맞는지 정확히 읽더라도, 바코드가 상자 안 물건을 제대로 설명하는지는 사람이 열어 대조해야 하는 것과 같다. Lean은 입력된 형식 명제가 논리적으로 증명되는지는 검사하지만, 그 명제가 원래 자연어 주장과 정확히 같은지, 결과가 새로운지, 중요한지, 선행 연구를 올바르게 인용했는지는 판단하지 않는다.

고등과학원 HORIZON이 소개한 자연수 뺄셈 사례도 이 차이를 보여준다. 뺄셈의 정의 차이 때문에 사람이 의도한 문제보다 쉬운 다른 명제가 Lean으로 형식화될 수 있다는 사례다. Lean 코드가 통과하는 것과 원래 자연어 명제가 그대로 검증됐다는 것이 같은 말은 아니라는 뜻이다. 다만 이 사례가 이번 철회 원고의 직접적인 오류 원인이었다는 근거는 없다.

증명 생산라인 뒤에 남은 인간의 품질관리실

Advisory Group on Mathematics and Artificial Intelligence(AGMAI)는 AI 생성 수학 결과의 책임 있는 공개 원칙을 마련하며 수학계로부터 600건 이상의 의견을 받았다고 밝혔다. 인간이 결과를 이해하지 못한 채 대량 공개할 경우 기업이 문헌 조사, 읽을 수 있는 서술, 형식화, 생성 정보 공개와 후속 인간 이해를 위한 지원을 책임져야 한다고 권고했다. 기업이 통제하지 않고 영구 식별자와 변경 기록, 논평 기능을 갖춘 학술 저장소를 활용할 것도 제안했다.

AGMAI는 OpenAI와 논의했지만, 그 자문이 원고의 정확성이나 중요성 또는 OpenAI의 절차를 승인한다는 뜻은 아니라고 선을 그었다. 공개는 인간의 이해와 수학 지식으로의 편입이 끝났다는 선언이 아니라 그 작업의 시작이라는 입장이다. 사용 모델의 구체적인 명칭과 가중치, 외부 접근권이 공개되지 않았고 대부분 원고의 전체 프롬프트와 생성 과정, 개별 계산비용도 공개되지 않아 제3자가 같은 실험을 반복하기 어렵다는 한계도 남았다.

한국에서도 이 문제를 다룰 기반은 만들어지고 있다. 한국과학기술원(KAIST) AI수학대학원은 2026학년도 봄학기부터 형식화 수학 개론, 대화형 정리 증명론, 자동 추론과 증명 탐색, 정리증명 인공지능, 인공지능 기반 수학 발견 등 5개 자체 선택과목을 교육과정에 편성했다. 공개 연구 주제에는 수학 명제 증명용 대규모언어모델 학습 데이터 생성과 여러 추측에 관한 계산·패턴 인식 및 반례 탐색 등이 포함됐다. 다만 국내 연구진이 OpenAI의 현행 719편을 공식적으로 전수 검증하고 있다는 근거는 확인되지 않았다.

이번 공개를 AI 수학의 성공이나 실패 한쪽으로만 판정하기는 이르다. 공개와 변경 기록은 외부 검토와 오류 수정의 출발점이며, 세 편의 철회만으로 나머지 결과의 가치를 부정할 수 없다. 반대로 세 편만 철회됐다는 사실이 나머지 원고의 정확성을 입증하지도 않는다. 분명해진 것은 증명 후보를 만드는 생산라인의 속도와 그것을 읽고 이해하며 검증하고 책임지는 품질관리실의 속도 사이에 큰 간격이 생겼다는 점이다. AI가 수학자의 일을 없앴다기보다, 수학자가 가장 많은 시간을 써야 할 지점을 ‘발견’에서 ‘검증과 이해’로 옮겨 놓은 사건에 가깝다.

자료: OpenAI·Advisory Group on Mathematics and Artificial Intelligence(AGMAI)·Lean·고등과학원·한국과학기술원(KAIST) AI수학대학원