OpenAI Astra 수학 증명 표절 의혹 정리 — Lean이 검증하지 못한 것

8월 1일 OpenAI가 논문 한 편을 냈다. 제목은 「Ten advances in mathematics and theoretical computer science」. 최소 10년 동안 아무도 진전을 못 낸 수학·이론 컴퓨터과학 문제 열 개를, 아직 공개되지 않은 내부 모델 Astra가 풀었다는 내용이다.

증명은 Lean 4로 형식화해 GitHub에 올렸다. 저장소의 sorry 개수는 0이었다. Lean에서 sorry는 "여기는 아직 안 채웠음"을 뜻하는 표시다. 0이라는 건 열 개 증명의 모든 단계가 기계 검증을 통과했다는 뜻이다.

그리고 열흘이 지나기 전에, 수학자들이 다른 이야기를 꺼냈다.

249페이지, 그리고 2,000달러

발표 내용부터 짚고 가자.

• 대상 문제 10개 — 최소 10년간 주요 결과에 진전이 없던 것들
• 원고 분량 약 249페이지
• Lean 4 증명 인증서를 Apache 2.0으로 공개, sorry 카운트 0
• 계산 비용 약 2,000달러

2,000달러라는 숫자가 특히 화제였다. 수십 년 묵은 난제를 커피값 수백 잔 값에 풀었다는 그림이 만들어졌으니까.

반응도 좋았다. 필즈상 수상자 티모시 가워스는 그중 한 증명을 최상위 저널에 주저 없이 추천하겠다고 했다. 에르되시 문제 데이터베이스를 운영하는 맨체스터대의 토머스 블룸은 "큰 뉴스"라며, 지난 5월 OpenAI가 공개한 에르되시 단위거리 추측 반증보다 이번이 더 중요하다고 평했다.

"그 논증은 2016년 내 논문에 있다"

제동을 건 사람은 예시바대의 수학자 스티븐 밀러다.

문제가 된 건 고차원 구 채우기(sphere packing) 결과였다. 밀러는 그 증명의 핵심 논증이 2016년 자신과 공동 연구자가 낸 논문에 이미 나온 것인데, Astra의 결과물은 그것을 마치 새로 만든 것처럼 제시했다고 주장했다.

그는 이걸 단순 실수로 보지 않았다.

"그들은 앞서 온 사람들의 연구를 의도적으로 짓밟고 있다"

밀러는 이를 연구 부정행위(research misconduct) 라고 규정했다.

두 번째 사례

지적은 하나로 끝나지 않았다. 케임브리지대의 군론 연구자 프란체스코 푸르니에-파시오는 소픽 군(sofic group) 관련 결과를 들여다봤다.

처음에는 새로워 보였다고 한다. 그런데 뜯어보니 2016년과 2019년 논문의 아이디어를 조합한 것이었고, 최초 발표문은 그 선행 연구들이 얼마나 결정적이었는지를 제대로 밝히지 않았다는 게 그의 지적이다.

OpenAI가 처음 배포한 보도자료에는 해당 문제들이 "최소 10년간 주요 결과에 진전이 없었다"는 표현이 있었다. 이 문장은 이후 더 정확한 쪽으로 수정됐다.

OpenAI의 답

OpenAI 대변인은 이렇게 답했다.

"우리는 이 결과들의 정확성에 책임을 지며, 인간 수학자에게 일반적으로 기대되는 것과 같은 기준을 충족하고 있다. 통상적인 학술 관행에 따라 이번 주에 소폭 수정할 계획이다."

정확성은 책임지겠다는 것이고, 표기는 손보겠다는 것이다. 의혹의 핵심인 "선행 연구를 알고도 뺐느냐"에 대한 직접적인 답은 아니었다.

귀속에 대한 회사 입장은 좀 더 흥미롭다. 원고와 형식화의 정확성은 자신들이 지되, 수학적 논증의 공은 모델에 돌려야 한다는 것이다. 회사는 "AI 시스템이 전적으로 생성한 증명에 인간 저자 지위를 주장하는 것은 시스템의 기여와 진짜 인간 지적 노동의 성격을 둘 다 왜곡한다" 고 밝혔다.

라이덴 선언을 인용하는 방식

여기서 한 번 더 짚을 대목이 있다.

2026년 6월, 수학자들이 라이덴 선언(Leiden Declaration on AI and Mathematics)을 내놨고 국제수학연맹이 이를 지지했다. 선언의 요지는 AI 기업들이 출판된 연구를 동의 없이 쓰고, 동료심사를 건너뛰고, 증명과 크레딧의 기준을 무너뜨린다는 경고였다.

OpenAI는 이 선언을 인용했다. 다만 방향이 달랐다. 선행 연구에 크레딧을 주라는 문서를, AI에게 크레딧을 주자는 근거로 끌어 썼다.

여기서 두 질문이 슬쩍 바뀐다. 밀러가 던진 질문은 "이 아이디어를 누가 먼저 생각했나"였다. OpenAI가 답한 질문은 "이 증명을 누가 썼나, 사람인가 기계인가"였다. 둘은 같은 질문이 아니다.

이번 일에서 진짜 흥미로운 지점은 어느 쪽이 옳으냐가 아니라, 자동화된 것과 자동화되지 않은 것의 경계가 선명하게 드러났다는 데 있다. Lean은 "이 증명이 맞는가"를 사람 없이 확인해준다. sorry 0은 그 답이 예라는 뜻이고, 그건 진짜 성취다. 그런데 Lean은 "이 아이디어가 처음인가"는 확인해주지 않는다. 그건 사람이 선행 문헌을 뒤져야 알 수 있는 일이고, 이번 논쟁은 정확히 그 자동화되지 않은 칸에서 터졌다. 정확성은 기계가 가져갔는데 독창성과 귀속은 여전히 사람 몫으로 남은 셈이다. 그래서 2,000달러라는 숫자도 다시 봐야 한다. 생성 비용은 그게 맞을지 몰라도, 249페이지를 읽고 수십 년 치 선행 문헌과 대조할 수 있는 사람은 분야마다 몇 명뿐이다. 검증의 병목은 값이 싸지지 않았다. 개발자에게 이 구조는 낯설지 않을 것이다. AI가 짜준 코드가 테스트를 통과하는 건 CI가 알려주지만, 그 코드가 어디서 온 조각인지, 라이선스가 뭔지는 아무도 알려주지 않는다. 수학에서 벌어진 일과 형태가 같다.

열 개 결과 가운데 동료심사를 마친 것은 아직 하나도 없다. 의미를 판정하는 절차는 이제 시작이다. 밀러와 푸르니에-파시오의 지적이 최종적으로 어떻게 정리되든, "AI가 새로운 수학을 하고 있다"는 문장이 성립하려면 넘어야 할 관문이 하나 더 생긴 것은 분명하다.

여러분은 어떻게 보시나요. AI가 만든 결과물에 선행 연구를 찾아 인용할 책임은 누구에게 있을까요 — 모델을 돌린 회사일까요, 아니면 그 결과를 쓰는 사람일까요?

---

📎 출처: 원문 보기