라떼군 뉴스


OpenAI, AI가 쓴 수학 논문 722편을 GitHub에 공개했다. Lean 문서가 붙은 묶음은 372개 중 235개다

OpenAI가 미공개 내부 모델이 만든 수학 논문 722편을 GitHub에 공개했습니다. 372개 묶음 가운데 컴퓨터가 증명을 검사하는 Lean 문서가 붙은 것은 235개입니다.

OpenAI에서 원문 읽기 ↗

수학에서 새 증명은 보통 다른 수학자들의 검토를 거쳐 학계에 받아들여집니다. 그런데 OpenAI는 10월 6일(미국 시간), 아직 공개하지 않은 내부 모델이 만든 수학 논문 722편을 GitHub에 한꺼번에 올렸습니다. 관련 논문끼리 묶으면 372개입니다.

OpenAI는 이 모델에 약 4,000개 문제를 풀게 한 뒤, 의미가 충분하다고 판단한 결과만 추렸다고 밝혔습니다. 결과 하나에 든 컴퓨팅은 평균적으로 ChatGPT Pro가 약 세 시간 생각하는 양에 해당합니다. Scientific American에 따르면 OpenAI는 거의 모든 결과가 에이전트 하나에 프롬프트 하나를 준 결과라고 설명했습니다.

결과를 확인하는 수단은 Lean입니다. Lean은 증명의 논리를 컴퓨터가 한 단계씩 검사하는 프로그래밍 언어입니다. 증명을 Lean으로 옮기면 사람이 읽지 않아도 논리가 맞는지 확인할 수 있습니다. OpenAI가 올린 논문 목록을 세어 보면 372개 묶음 가운데 Lean 문서가 붙은 것은 235개이고, 붙지 않은 것은 137개입니다. Lean으로 옮기지 않은 결과에는 문제가 있을 수 있다고 OpenAI도 밝혔습니다.

예외도 있습니다. OpenAI는 리만 제타 함수의 영점이 없는 영역에 관한 연구와, 호지 추측을 특수한 경우에서 증명한 결과를 나머지와 다른 절차로 얻었다고 밝혔습니다. 둘 다 이름난 난제와 이어진 주제입니다. 제타 함수 쪽 글은 읽기 쉽도록 사람이 고쳤습니다.

다른 사람이 같은 방식으로 결과를 다시 만들어 볼 수는 없습니다. 모델을 공개하지 않았고 프롬프트도 밝히지 않았기 때문입니다. OpenAI가 조언을 구한 고등연구소(IAS)의 수학과 AI 자문단은 모델, 정확한 프롬프트, 문제별 컴퓨팅 시간을 공개하라고 권고했습니다. Scientific American에 따르면 OpenAI가 밝힌 정보는 평균 컴퓨팅 시간과 몇 가지 통계뿐입니다. MIT의 Andrew Sutherland는 모델이 공개되고 결과가 재현되기 전까지 에이전트 하나가 한 번에 풀었다는 주장을 검증되지 않은 것으로 봐야 한다고 말했습니다.

이제 이 소식을 읽는 기준도 달라져야 합니다. 지금까지는 AI가 어려운 문제를 풀었다는 사실 자체가 소식이었습니다. 하지만 722편이 한꺼번에 나오면, 풀었다는 주장보다 누가 그 주장을 어디까지 확인했는지가 먼저 궁금해집니다.

개발자에게도 낯익은 장면입니다. AI가 올린 풀 리퀘스트에 테스트와 타입 검사가 붙어 있으면 기계가 먼저 걸러 줄 수 있지만, 검사가 없으면 사람이 처음부터 읽고 판단해야 합니다. AI에게 일을 맡길 때는 결과가 맞는지 자동으로 확인할 검사도 함께 만들 수 있는지 따져야 합니다.

다만 Lean도 모든 것을 보증하지는 않습니다. Lean이 확인하는 범위는 증명이 내세운 명제를 올바르게 증명했는지까지입니다. 그 명제가 원래 문제를 제대로 옮긴 것인지는 사람이 따로 살펴야 합니다. 테스트가 통과했다고 요구사항까지 만족한다고 단정할 수 없는 것과 같습니다.

그래서 AI가 낸 결과를 믿을 수 있는지는 얼마나 많이 나왔느냐보다 무엇까지 확인했느냐에 달릴 것입니다. AI에게 일을 맡길 때는 결과를 받기 전에, 기계가 무엇을 확인해 주고 사람이 무엇을 읽어야 하는지부터 정해 두는 것이 첫걸음입니다.

출처

  1. OpenAI: Sharing AI progress in mathematics, 2026년 10월 6일. 이 페이지는 자동 접근이 막혀 같은 발표 내용을 올린 3번과 2번으로 대조했습니다.
  2. OpenAI: openai/math 저장소, 2026년 10월 6일. README, 논문 목록(CONTENTS.md), Lean 형식화 목록(lean/formalization.yaml). Lean 문서가 붙은 묶음 235개는 논문 목록의 Lean 링크를 직접 센 값입니다.
  3. OpenAI 커뮤니티: First look at mathematics manuscripts from an internal frontier model at OpenAI, 2026년 10월.
  4. Scientific American: OpenAI unleashes hundreds more math results upon a field already in shock, 2026년 10월 6일. Joseph Howlett 작성.

함께 생각해 볼 질문

우리 서비스에서 AI에게 맡기는 일 가운데, 결과가 맞는지 기계가 판정해 줄 수 있는 일은 얼마나 될까요?

메일로 새 글 받기

새로 고른 뉴스를 메일로 보내 드립니다. 받은 메일의 링크에서 언제든 구독을 해지할 수 있습니다.

RSS로 새 글 받기

RSS 리더에 피드 주소를 추가하면 새 글을 모아 볼 수 있습니다.

피드 열기 ↗