AI 수학 스타트업 액시엄매스가 소수 간격에 관한 현존 최강 정리인 '246 정리'(무한히 많은 소수 쌍의 차이가 246 이하)를 린(Lean) 4로 기계 검증했다고 2026년 8월17일 발표했다. 이 결과는 제임스 메이너드의 2013년 논문과 폴리매스8b 공동연구의 후속 성과를 통합 형식화한 것으로, 액시엄프루버라는 다중 에이전트 시스템이 초안 증명을 생성하고 41명의 연구·엔지니어링 기여자가 검토·구성했다. 소수 간격 상한은 2013년 장이탕의 7000만에서 메이너드의 600, 이후 폴리매스8b의 246까지 좁혀져 온 역사가 있으며, 이번 성과는 단발성 증명이 아니라 향후 연구에 재사용 가능한 라이브러리 '프라임갭스립'을 구축했다는 점에서 의미가 크다. 창립 수학자 켄 오노는 이번 작업이 향후 AI 생성 코드 검증이라는 더 큰 과제의 시험대라고 평가했다.

• •액시엄매스, 소수 간격 246 정리를 린(Lean)4로 기계 검증한 공개 라이브러리 '프라임갭스립' 발표
• •2013년 장이탕의 7000만→메이너드 600→폴리매스8b 246으로 이어진 소수 간격 연구 성과를 형식화
• •다중 에이전트 시스템 액시엄프루버가 초안 생성, 41명 기여자가 검토
• •단발성 증명이 아닌 재사용 가능한 라이브러리 구축이 핵심 차별점
• •창립자 케 오노, 이번 작업을 AI 생성 코드 검증이라는 더 큰 과제의 시험대로 제시