Axiom Math의 AI가 Lean에서 246 소수 간격 정리를 검증

Axiom Math는 AxiomProver 시스템이 소수 사이 간격에 관한 현재 알려진 가장 강력한 결과인, 소수 쌍이 246 이하의 차이를 갖는 무한히 많은 경우가 존재한다는 정리의 Lean 4 기계 검증 증명을 만들었다고 발표했습니다. 이 회사는 2026년 8월 17일에 41명의 수학자, 엔지니어 및 주요 연구자에게 크레딧을 부여한 인터랙티브 형식화 청사진으로 결과를 공개했으며, IEEE Spectrum이 최초로 이 이정표를 보도했습니다.

246 제한은 쌍둥이 소수 추측에 대한 오랜 연구에서 인간 지식의 현재 최전선입니다. 이 추측은 19세기에 Alphonse de Polignac이 정확히 차이가 2인 소수가 무한히 존재한다는 가설로 정식화한 것입니다. Axiom Math의 프로젝트 페이지는 이 작업을 James Maynard의 2013년 논문 “Small gaps between primes”(소수 사이의 작은 간격)와 Polymath8b 협업의 후속 작업을 통합한 형식화라고 설명합니다. 이 후속 작업은 Maynard가 제시한 600 제한을 246으로 강화했습니다. 기계 검증된 증명은 공개 Lean 라이브러리인 PrimeGapsLib에 정리되었으며, 246 정리가 그 대표 결과입니다.

“이 정리는 현재 소수에 대한 인간 지식의 한계를 나타냅니다.”라고 Axiom Math의 설립 수학자 Ken Ono가 말했습니다.

형식 검증이란 증명을 작은 신뢰받는 프로그램인 커널이 한 줄씩 검사할 수 있는 언어로 번역하는 것을 의미합니다. 결과가 절대적인 보장을 의미하는 것은 아니며—명제가 올바르게 번역되어야 하고, 검증기가 정확해야—but 인간 심판자의 오류 가능성을 체인에서 제거합니다. 지금까지 수학 벤치마크에서 경쟁하는 AI 시스템은 주로 짧고 자체 포함된 증명을 가진 경쟁 문제에 대해 평가되었으며, 이러한 결과와 연구 수준 형식화 사이의 격차는 크게 벌어져 왔습니다. 이는 올림피아드 기하학에서 뛰어난 성과를 보였던 이전 시스템에서도 확인되며, 연구 수학은 대부분 손대지 않은 상태였습니다.

70백만에서 246까지

이 추측 자체는 19세기 Alphonse de Polignac이 정확히 공식화했지만 아직 증명되지 않았습니다. 최초의 유한 제한은 2013년에 Yitang Zhang가 무한히 많은 소수 쌍이 7천만 이내에 존재한다는 것을 증명하면서 등장했습니다. 몇 달 뒤 Maynard는 정제된 체 체법을 도입해 제한을 600으로 낮췄으며—이 작업은 그의 2022년 필즈 메달 수상에 기여했습니다—그리고 Maynard와 Terence Tao가 참여한 Polymath8b 협업은 이를 246으로 끌어냈습니다. Axiom Math의 청사진은 이 진행 과정을 프로젝트가 형식화하려는 목표로 제시합니다.

형식화는 회사가 세 단계로 설명하는 파이프라인을 따릅니다. 연구자들은 먼저 증명을 청사진 형태로 작성했으며—각 정의, 보조정리, 정리마다 라벨, 정확한 진술, 그리고 의존하는 결과 목록을 부여해 작업 순서를 나타내는 의존 그래프를 만들었습니다. 그런 다음 AxiomProver, 즉 형식 증명을 통한 수학 연구를 위한 다중 에이전트 시스템이 Mathlib(커뮤니티 수학 라이브러리)와 Alex Kontorovich와 Tao가 이끄는 기존 형식화 프로젝트 PrimeNumberTheoremAnd 위에 구축된 기계 검증 가능한 Lean 4 증명을 생성했습니다. Axiom 팀은 생성된 코드를 검토하고 이를 PrimeGapsLib에 정리했습니다.

라이브러리가 명시한 주요 결과는 헤드라인 정리보다 약간 더 넓습니다. 246 제한과 함께 Maynard의 600 제한도 형식화했으며, Mathlib만을 기반으로 하고 증명 슬롯을 비워 둔 자체 검증 챌린지도 포함합니다. 이를 통해 Lean 비교 도구를 가진 누구든지 라이브러리의 증명이 명시된 정리와 일치하는지 독립적으로 확인할 수 있습니다. 회사는 전체 검증에 몇 시간이 걸릴 수 있다고 경고하지만, 다른 두 결과만을 포함한 축소 버전은 몇 분 안에 실행된다고 밝혔습니다.

AI 형식화 주장 중 이 위치

이 결과는 AI 시스템이 연구 수준 수학을 수행한다는 주장이 급증하고 있는 시기에 등장했으며, 대부분은 경쟁 점수나 짧은 증명에 근거하고 있습니다. Axiom Math는 가장 공격적인 주장자 중 하나이며—AxiomProver는 이전에 열려 있던 문제들을 해결한 공로를 인정받았으며, 회사가 동료 검토 저널에 게재한 작업도 포함하고, AI 시스템이 이제 여러 오래된 Erdős 문제들을 해결했다—를 내세웁니다. 246 형식화는 새로운 정리가 아니라 현대 수론에서 가장 기술적으로 까다로운 증명 중 하나를 기계 검증한 재구성이라는 점에서 다른 종류의 결과입니다.

가장 가까운 비교는 올해 초, Math, Inc.가 Gauss 에이전트를 사용해 Maryna Viazovska가 8차원과 24차원에서 필즈 메달을 수상한 구체 포장 결과의 형식 증명을 완성한 경우였습니다. Carnegie Mellon 대학 박사과정 학생이자 그 형식화의 인간 청사진 작업을 이끌었으며 현재 Axiom Math 인턴이자 246 프로젝트의 명시된 수학 기여자인 Sidharth Hariharan은 새로운 결과가 더 포괄적인 성취라고 주장합니다. 그의 논리에 따르면 Axiom은 재사용을 위해 구축되었습니다: 단일 증명의 일회성 형식화가 아니라, PrimeGapsLib는 향후 형식화 작업과 연구를 지원하도록 유지 관리되는 소수 간격 결과 라이브러리입니다.

이 구분은 결과를 어떻게 읽어야 하는지에 영향을 미칩니다. 일회성 검증은 시스템이 하나의 어려운 증명을 처리할 수 있음을 보여줍니다. 반면 라이브러리는 인프라에 더 가까운 것을 보여줍니다—다른 결과가 기반으로 할 수 있는 재사용 가능한 형식 기계이며—이는 형식 증명 시스템이 연습 문제 해결에서 실제 수학 검증으로 전환하고 있는 방향과 일치합니다. 여기서의 역량 주장은 벤치마크 점수가 아니라 공개되고 재실행 가능한 산출물—청사진, Lean 코드, 그리고 외부 연구자들이 스스로 증명을 검증할 수 있도록 설계된 비교 챌린지—에 기반합니다.

Ono는 수학을 더 큰 야망을 위한 시험대로 제시합니다. 소프트웨어의 특성—프로그램이 종료되는지, 모든 입력에 대해 출력이 정확한지—을 정확한 수학적 명제로 표현할 수 있다면, AxiomProver에서 파생된 시스템이 이를 형식적으로 증명할 수 있다고 그는 주장하며, 이는 인프라, 금융, 보안 시스템을 운영하는 AI 생성 코드의 검증을 향한 방향을 가리킨다고 말합니다.

“세상은 이제 아무도 읽지 않은 컴퓨터 코드 위에서 돌아가게 될 것입니다,”라고 Ono가 말했습니다. “AI는 이미 여기 있으며 우리는 더 이상 외면할 수 없습니다—증명 형식화는 AI가 제시하는 가장 중요한 과제라고 생각하는 문제를 해결하기 위한 시험대입니다.”

현재 제공되는 결과물은 더 좁고 검증 가능한 형태입니다: 41명의 저자가 참여한 청사진, 공개 Lean 라이브러리, 그리고 246 이내에 있는 소수 쌍이 결코 소진되지 않음을 증명하는 기계 검증 증명—쌍둥이 소수 추측의 가장 가까운 검증된 이웃이며, AI 시스템이 지금까지 끝까지 검증한 가장 깊은 연구 수학 결과입니다.