Aaronson-Ambainis 추측: AI가 18년 된 양자 퍼즐을 3일 만에 증명하다

11월 6일, Physical Superintelligence(PSI)라는 작은 회사가 10년 전이라면 공상과학처럼 들렸을 발표를 했다. 비공개 Anthropic 모델을 실행하는 AI 연구 시스템이 2008년부터 미해결이던 양자 복잡도 이론의 핵심 미해결 문제, Aaronson-Ambainis 추측을 증명했다는 것이다. 시스템은 실행 3일째에 완전한 증명을 확보했다. 모든 논리 단계를 기계로 검증하는 증명 보조 도구 Lean이 이를 받아들였다. PSI는 이후 시스템을 관련 문제들에 투입해 결과를 두 차례 개선하고, 논문과 공개 Lean 형식화를 함께 발표해 누구나 그 작업을 다시 검증할 수 있게 했다.

이것이 왜 중요한지 이해하려면 양자 컴퓨터가 실제로 잘하는 것부터 시작해야 한다. 1994년 피터 쇼어는 알려진 어떤 고전적 방법보다 훨씬 빠르게 큰 수를 인수분해하는 양자 알고리즘을 발견했다. 그러나 쇼어의 가속은 드문 행운에 의존한다. 문제 속에 반복 패턴이 숨어 있고, 양자 컴퓨터가 그 반복 빈도를 찾아내는 것이다. 알려진 대부분의 극적인 양자 가속도 같은 방식으로 작동한다. 구조를 이용하는 것이다.

스콧 애런슨과 안드리스 암바이니스는 불편한 질문을 던졌다. 그런 구조를 거의 절대 갖지 않는 무작위 입력은 어떤가. 양자 컴퓨터는 무작위 문자열에 대한 예·아니오 질문에 일반 컴퓨터보다 지수적으로 적은 횟수로 비트를 읽어 답할 수 있는가. 그들은 다항식에 관한 추측—순수 수학—을 제시하고, 그것이 참이라면 답은 아니오임을 보였다. 무작위 입력에서는 양자 컴퓨터가 다항식 배만큼 빠를 뿐이다. 이 추측은 양자 복잡도 이론의 핵심 미해결 문제 중 하나가 되었고, 2026년 8월 스탠퍼드 그룹이 특수한 경우—입력을 고정된 횟수의 병렬 라운드로 읽는 양자 알고리즘—에 대해 이를 증명했다.

PSI의 증명은 샤차르 로벳과 지아펑 장이 제시한 계획을 따르며, 그들의 계획에서 추측으로 남겨두었던 부등식 하나를 원고에서 증명된 새로운 부등식으로 대체한 것으로, 데이비드 라이머의 나비 보조정리(Butterfly Lemma)에 기반한 짝짓기 논증과 여러 다른 그룹의 결과를 이용했다. 과정에 참여한 인간, PSI의 데이비드 터투린은 연구 시스템을 구축하고 문제를 정하고 실행했으며 논문의 정확성에 책임을 진다. 고문 짐 할버슨이 증명을 감사했다. 특수한 경우를 증명한 스탠퍼드 그룹은 완전한 증명을 읽고 의견을 보냈으며 전문가를 위한 더 짧은 해설을 집필 중이다. 지금까지 그들의 평가는 "이것은 거대한 결과이다"라는 것이다.

이것이 이 뉴스를 읽는 올바른 방식이다. 대관식으로가 아니라 검증 가능한 결과물을 갖춘 주장으로. Lean의 수용은 높은 기준이다. 기계가 논증의 모든 단계를 검증한 것이다. Lean이 검증할 수 없는 것은 형식화된 명제가 수학자들이 실제로 관심 갖는 명제인지, 혹은 형식화 과정에서 숨은 가정이 몰래 들어갔는지 여부다. 그것은 인간 전문가의 일이며 아직 끝나지 않았다. 동료 심사는 이루어지지 않았다. 증명을 찾아낸 모델은 공개되지 않았으므로 누구도 발견 과정 자체를 다시 실행할 수 없다. 그것이 만들어낸 것을 검사할 수 있을 뿐이다.

그리고 이 발표가 나온 그 주가 바로 진짜 이야기다. PSI의 증명은 고립된 사건이 아니다. 10월에 OpenAI는 AI가 작성한 722편의 수학 원고를 공개했는데, 그중에는 준 리만 가설, 유일 게임 추측, 그리고 특정한 종류의 도형에 대한 호지 추측의 증명 주장이 포함되어 있다. 9월에는 Quarterly Journal of Mathematics의 논문이 AI 시스템이 k-미분에 관한 조건부 결과를 무조건 정리로 바꾸는 핵심 아이디어를 찾아냈으며, 결정적 보조정리가 Lean으로 형식적으로 증명되었다고 보고했다. Axiom은 약 7,500쪽—약 1,600만 행—의 Stacks Project를 형식화해 방대한 대수기하학을 기계로 검증 가능하게 만들었다. 패턴은 이제 명백하다. AI가 제안하고 Lean이 판정한다. 병목은 증명의 발견에서 증명의 검증으로 이동했고, 검증의 속도를 정하는 것은 여전히 인간이다.

내가 주목하는 것은 바로 이 전환이다. 스탠퍼드의 해설이 깔끔하게 나오고 다른 그룹이 결함을 찾지 못한다면, Aaronson-Ambainis 증명은 한 달 안에 전문가의 정밀 검사를 살아남은 두 번째 주요 AI 주장 결과가 된다. 그러면 질문은 AI가 최첨단 수학을 할 수 있는지가 아니라 검증 파이프라인이 얼마나 빨리 따라갈 수 있는지가 된다. 내 예측은 이렇다. 2027년 12월 31일까지 이 증명은 독립적인 수학자들에 의해 공개적으로 확인될 것이다. 스탠퍼드 그룹의 해설, 동료 심사 학술지 게재, 혹은 그에 준하는 공개 전문가 확인을 통해, 증명에서 실질적인 결함이 발견되지 않은 채로. 확률은 65%로 본다. 기계적 기준은 이미 통과했고 적절한 전문가들이 이미 참여하고 있지만, 인간의 확인은 형식이 아니며, 정의 하나의 불일치가 Lean으로 검증된 증명을 여전히 무너뜨릴 수 있기 때문이다.