AI가 만든 수학 연구 722편의 목록과 Lean 증명 공개

배경과 문제

새로운 수학 연구 결과를 평가하려면 정답이 정해진 시험 문제보다 넓은 범위의 문제와 검증 절차가 필요하다. OpenAI는 내부 프런티어 모델을 개방형 연구 문제에 적용했고, 기존 수학 평가에서 성능이 포화되자 평가 범위를 넓혔다고 밝힌다. 이번 공개는 그 과정에서 나온 원고를 수학계가 살펴볼 수 있도록 공개한 단계다.

공개 방식 자체도 문제였다. 단순히 결과 파일만 올리면 수학자들이 검증하거나 인용하기 어렵고, 어떤 과정으로 나왔는지 알 수 없어 신뢰가 떨어진다. 그래서 OpenAI는 고등연구소(IAS)의 '수학과 인공지능 자문단'과 협의해 모범 사례를 만들고, 그 권고를 반영해 GitHub 저장소 형태로 발표했다. 저장소에는 원고뿐 아니라 인용 정보, 수정 이력, 일부 증명의 컴퓨터 검증 코드가 함께 담겨 있다.

기존 접근의 한계

벤치마크가 포화되면 그 점수만으로 새로운 연구 문제를 다루는 능력을 가늠하기 어렵다. 또 개별 결과 파일만으로는 관련 논증의 관계나 검증 상태를 파악하기 어렵다. 이번 저장소는 722편의 원고를 372개 패밀리로 묶고 분야별로 분류했다. 이 수치는 서로 완전히 독립된 난제 722개를 해결했다는 뜻이 아니다. 한 패밀리에 주요 결과와 보조 논증, 따름정리, 대안 증명이 함께 들어갈 수 있다.

증명 검증의 어려움도 크다. 미세한 오류가 결론을 무너뜨릴 수 있으므로, 원고가 많다는 사실과 내용이 옳다는 판단은 별개다. OpenAI는 일부 증명을 Lean으로 형식화했다고 밝혔다. Lean은 명제와 가정을 명시한 코드 안에서 증명이 논리 규칙에 맞는지 검사하는 도구다. 형식화한 명제가 원래 연구 주장과 정확히 일치하는지, 결과가 새로운지는 별도로 살펴야 한다. 모든 원고가 형식화된 것은 아니며, 원문도 아직 형식화하지 않은 결과에는 문제가 있을 수 있다고 인정한다.

연구방법을 단계별로

첫 단계는 문제 선정이다. OpenAI는 내부 모델을 개방형 연구 문제에 적용했고, 기존 수학 평가에서 성능이 포화되자 평가 범위를 확장했다. 저장소 안내문에 따르면 평가 과정에서 모델에 약 4,000개의 문제를 제시했다. 이 중에서 유의미한 수준의 결과를 골라 주제별로 묶고 원고로 정리한 것이 이번 카탈로그다.

두 번째 단계는 결과 생성이다. 대다수 결과는 공개되지 않은 내부 OpenAI 모델로 같은 절차를 거쳐 얻었다. 평균적으로 한 결과당 ChatGPT Pro 사고 모드 약 3시간에 해당하는 계산을 사용했다고 한다. 다만 리만 제타 함수의 영점 없는 영역에 관한 연구와 CM 아벨 다양체에 대한 호지 추측 증명은 이 고정 절차의 예외로 명시되어 있다. 또 리만 제타 함수의 Re(s) > 11/12 영역 결과는 가독성을 위해 사람이 편집했다고 밝혔다.

세 번째 단계는 검증과 정리다. 결과를 372개 '패밀리'로 묶었는데, 한 패밀리는 주요 결과와 보조 논증, 따름정리, 대안 증명 등을 포함한다. 각 패밀리는 수학 분야별로 분류되어 있다. 일부 증명은 Lean으로 형식화해 컴퓨터 검증을 받았고, 나머지는 형식화가 진행 중이거나 아직 되지 않았다. 원문은 형식화되지 않은 결과에 문제가 있을 수 있으며, 발견되면 신속히 수정하겠다고 밝혔다.

마지막 단계는 투명성 자료 제공이다. 모델의 추론을 요약한 10개의 문서, ChatGPT Pro 사용량으로 환산한 계산 비용 추정치, 시도한 문제 수 통계를 저장소에 포함했다. 예를 들어 추론 요약에는 'π의 무리성 지수', '대칭 및 일반 말러 추측', '자유군 인자 동형 문제' 등이 포함되어 있다. 이는 연구자가 결과의 배경을 이해하고 재현 가능성을 평가하는 데 도움을 주기 위한 것이다.

결과와 숫자의 의미

가장 눈에 띄는 숫자는 722편의 원고와 372개 패밀리다. 이는 단순히 많은 결과를 나열한 것이 아니라, 관련 결과를 묶어 하나의 주제로 이해할 수 있게 한 구조다. 예를 들어 '수론' 분야에는 밀른의 유리성 추측, 버치-스위너턴다이어 공식, 준 리만 가설, 힐베르트의 10번째 문제 등이 포함되어 있다. 각 패밀리에는 주요 논문과 함께 보조 논문이 연결되어 있어, 한 결과가 다른 결과를 어떻게 뒷받침하는지 볼 수 있다.

저장소는 결과 하나에 사용된 계산량이 평균적으로 ChatGPT Pro의 사고 모드 약 3시간에 해당한다고 추정한다. 이는 실제 경과 시간이나 지불 비용의 측정값이 아니다. 약 4,000개 문제를 시도했다는 통계와도 분모가 다르다. 실패한 시도나 여러 원고로 이어진 결과의 계산을 어떻게 배분했는지 충분히 설명하지 않으므로, 두 숫자를 곱해 총비용을 구하거나 인간 연구 시간과 속도를 비교할 수 없다.

검증 수준은 결과마다 다르다. Lean 검증 여부는 해당 코드의 명제와 가정까지 함께 확인해야 하며, 형식화되지 않은 결과는 증명 자체를 검토해야 한다. 따라서 722편 전체를 같은 검증 상태로 취급할 수 없다. 이 설명은 공개 안내문·카탈로그·Lean 안내를 확인한 것이며, 개별 논문 전체를 읽거나 Lean 라이브러리를 직접 빌드해 검증한 결과가 아니다.

구체적인 예시

추론 요약이 공개된 사례에는 「π의 무리성 지수」가 있다. 무리성 지수는 무리수를 분수로 얼마나 잘 근사할 수 있는지를 나타낸다. 카탈로그는 π의 무리성 지수가 정확히 2라는 결과를 제시한다. 비전공자에게는 π를 분수로 근사하는 정확도에 특정한 한계를 설정하는 주장이라고 이해할 수 있다. 여기서는 해당 개별 증명을 검토하지 않았으므로, 이 수학적 결론은 카탈로그의 주장으로 소개한다.

「대칭 및 일반 말러 추측」도 포함되어 있다. 말러 추측은 볼록한 물체의 부피와 그 쌍대 물체 부피의 곱이 얼마나 작아질 수 있는지 묻는다. 카탈로그는 모든 차원에서의 해결과 등호 성립 경우를 제시한다고 설명한다. 독자는 이 항목을 출발점으로 개별 원고, 가정, 관련 보조 논증과 형식화 상태를 확인할 수 있다. 목록에 실렸다는 사실만으로 검토가 끝났다고 해석하면 안 된다.

컴퓨터 과학 분야에는 「기본 반정부호 임계값에서의 NP-난해성」이 있다. 카탈로그는 특정 최적화 문제를 어느 수준 이상 근사하는 어려움과 관련된 결과로 소개한다. 이런 예시는 공개 목록이 수론·기하학·컴퓨터 과학 등 여러 분야에 걸쳐 있음을 보여준다. 다만 분야별로 어떤 문제를 얼마나 시도하고 성공했는지는 별도의 평가가 필요하다.

한계와 오해하기 쉬운 점

가장 큰 한계는 검증의 불완전성이다. Lean 형식화가 모든 원고에 적용된 것은 아니며, 형식화되지 않은 결과는 오류가 있을 수 있다. 원문은 '일부 형식화되지 않은 결과에는 문제가 있을 수 있다'고 명시하고, 문제를 발견하면 신속히 수정하겠다고 밝혔다. 따라서 이번 공개를 '모든 결과가 증명되었다'고 받아들이면 안 된다. 각 결과는 검증 단계가 다르며, 수학계의 독립적인 검토가 필요하다.

또한 이 글의 입력에는 개별 논문 722편의 본문과 전체 Lean 코드가 포함되어 있지 않다. 따라서 특정 정리의 증명이 실제로 올바른지, Lean 코드가 정확히 어떤 명제를 검증하는지는 이 글만으로 확인할 수 없다. 이번 설명에서 확인한 범위는 공개 문서가 전하는 결과와 검증 안내이며, 개별 결과의 수학적 타당성은 별도 검토가 필요하다.

계산량의 환산값만으로 재현 비용을 알 수는 없다. 사용 모델이 공개되지 않았고, 모델의 추론 요약도 전체 실행 기록은 아니다. 평균적인 계산 규모에 관한 참고 자료는 있지만, 독자가 같은 모델과 절차로 결과를 그대로 재현할 수 있다는 보장은 없다.

사람의 관여 정도도 결과별로 구분해야 한다. 원문은 리만 제타 함수의 Re(s) > 11/12 영역에 관한 원고를 가독성을 위해 사람이 편집했다고 명시하고, 대다수 결과에 사용한 고정 절차의 예외도 따로 밝힌다. 그 설명을 전체 원고가 같은 방식으로 편집되었다는 뜻으로 확대할 수 없다. OpenAI는 수학계의 피드백에 따라 공개 관행을 개선하겠다고 밝히고 있다.

실제로 어떻게 활용할까

수학 연구자는 관심 분야의 패밀리에서 시작해 주요 원고와 보조 논증을 연결해 읽고, 각 디렉토리의 Lean 형식화 상태와 BibTeX 인용 정보를 확인할 수 있다. OpenAI는 공개 이력을 보존하고 수정 사항을 새 버전으로 남기겠다는 방침을 밝혔다. 인용하거나 후속 연구에 사용할 때는 어느 버전의 주장과 증명을 확인했는지 기록하는 것이 유용하다.

컴퓨터 검증에 관심 있다면 저장소의 Lean 안내를 따라 관심 결과의 작은 부분부터 살펴볼 수 있다. 안내문은 전체 라이브러리를 한 번에 빌드할 때 생길 수 있는 자원·환경 문제도 설명한다. 코드가 빌드되는지뿐 아니라, 검증 대상 명제와 가정이 자신이 읽은 원고의 주장에 대응하는지 확인하는 것이 핵심이다.

AI 연구자에게는 모델의 추론 요약 10개가 유용한 자료다. 이 요약들은 모델이 어떤 방식으로 문제에 접근했는지 엿볼 수 있는 창구다. 다만 '요약'이므로 전체 추론 과정이 아니라 압축된 버전이며, 원문은 이를 'abridged summaries'라고 명시한다. 따라서 모델의 사고 과정을 완전히 재구성하려는 목적에는 한계가 있다.

교육적으로는 이번 공개가 '컴퓨터 지원 수학 연구'의 실제 사례를 제공한다. 학생이나 일반 독자는 특정 패밀리의 개요를 읽고, 그 결과가 어떤 분야의 어떤 문제를 해결했는지 파악할 수 있다. 다만 개별 원고는 전문적인 수학 지식이 필요하므로, 비전공자는 overview.pdf의 패밀리 설명부터 시작하는 것이 좋다.