구글 AI가 56년 미해결 수학 난제를 수백 달러에 풀었다

구글 딥마인드의 한 연구 시스템이 수학자 폴 에르되시(Paul Erdős)가 제기한 아홉 개의 미해결 문제에 대해 기계로 검증된 완전한 증명을 내놓았다. 그중 둘은 56년 동안 풀리지 않았다. 같은 시스템은 정수열 온라인 백과사전에서 가져온 44개의 추측을 정리했고, 15년 동안 열려 있던 대수기하학의 물음을 닫았으며, 볼록 최적화의 알려진 상한을 개선했다. 눈길을 끄는 숫자보다 방법이 중요하다. 이 증명들은 하나하나가 기계의 주장에 그치지 않고 기계로 검증되었다.

1996년에 세상을 떠난 에르되시는 정확하고 고집스러운 물음을 수백 개 남겼다. 많은 것이 말하기는 쉬워도 결판내기는 끔찍하게 어렵다. 수십 년에 걸쳐 그것들은 이 분야의 상설 시험처럼 되었다. 수열 추측은 수학자들이 규칙을 찾아 파헤치는 공개 데이터베이스에서 나오며, 짐작한 공식이 몇 년이고 증명되지 않은 채 남기도 한다. 모델을 띄워주려고 꾸민 인위적 과제가 아니다. 열린 수학의 진짜 밀린 숙제다.

이 구분이 이야기의 전부다. AlphaProof Nexus라 불리는 이 시스템은 확인할 수 없는 단계를 모두 거부하는 형식 언어 Lean으로 논증을 쓴다. 증명은 통과하거나 못 하거나 둘 중 하나이며, 나중에 틀린 것으로 드러나는 자신만만한 문단이 끼어들 여지가 없다. AI의 ‘발견’이 진짜인지 가리려는 사람에게는, 이것이 보도자료와 결과를 가르는 경계선이다.

추천 읽을거리딥시크가 AI를 싸게 만들었다, 미국 AI 거품은 그 반대에 베팅했다

내부에서 증명기는 Gemini 3.1 Pro 위에서 돌아가고, 더 가벼운 모델이 순위 매기기를 맡는다. 순환 과정은 거의 지루할 정도다. 모델이 Lean으로 증명을 쓰고, 컴파일러가 오류를 돌려주며, 그 오류가 다음 시도로 흘러든다. 정직함을 지키는 것은 매끄러운 문장이 아니라 기호적 피드백이다. 연구진은 복잡도가 점점 높아지는 네 가지 판본을 만들었고, 그중 하나는 경쟁하는 증명 초안을 만들고 순위를 매긴다. 그런데도 가장 단순한 판본, 모델과 컴파일러만의 순환이 아홉 개의 에르되시 문제를 혼자 풀었다.

조용히 놀라운 대목은 비용이다. 풀린 문제 하나마다 계산 시간으로 수백 달러가 들었다. 연구자의 평생을 삼킨 물음이 주말 여행쯤의 값에 닫혔다. 그렇다고 수학자가 은퇴하는 것은 아니다. 어떤 문제가 도전할 가치가 있는지 고르고, 시스템이 읽을 수 있는 형태로 다듬고, 답이 무엇을 뜻하는지 판단하는 일은 여전히 사람의 몫이다. 달라지는 것은 애초에 무엇을 시도할 가치가 있는가라는 셈법이다.

단서는 표제보다 무겁다. 시도한 353개의 에르되시 문제 가운데 아홉 개 성공은 약 2.5퍼센트의 적중률이다. 수열 쪽 숫자인 492개 중 44개는 9퍼센트에 못 미친다. 저자들은 이 문제들의 대다수가 여전히 손이 닿지 않는 곳에 있으며, 광범위한 새 이론을 요구하는 것은 더더욱 그렇고, 성공은 Lean의 수학 라이브러리가 이미 두꺼운 영역에 몰려 있다고 거리낌 없이 인정한다. 사람이 쌓은 그 발판과 엄선된 표적 목록을 걷어내면, 시스템에는 디딜 땅이 거의 남지 않는다.

신중함에는 까닭이 있다. 크게 조롱당한 일화에서, 경쟁 연구소는 자사 모델이 열 개의 에르되시 문제를 풀었다고 발표했지만, 수학자들은 그 답이 이미 출판된 문헌에 있었다고 지적했다. 모델은 그것을 찾아냈을 뿐, 증명한 것이 아니었다. AlphaProof Nexus는 그 실수에 면역이 되도록 만들어졌다. 알려진 결과의 Lean 증명도 여전히 유효한 증명이고, 정말로 새로운 것의 Lean 증명은 꾸며낼 수 없다. 딥마인드를 이끄는 데미스 허사비스(Demis Hassabis)는 이 작업이 범용 인공지능이 아니라고 굳이 못 박았다. 자사 모델에 좀처럼 조심스럽지 않은 회사로서는 이례적으로 신중한 토다.

연구진이 강조하는 더 미묘한 소득도 있다. 실패조차 쓸모가 있었다. 부분 증명이 모두 형식적으로 검증되기 때문에, 수학자들은 논증 전체를 손으로 다시 확인하지 않고도 시스템이 어떤 하위 목표를 닫을 수 있고 어떤 것을 닫지 못하는지 정확히 볼 수 있었다. 기계는 신탁이기를 멈추고, 자기 작업을 보여주며 어려운 대목이 아직 어디 숨었는지 가리키는 지칠 줄 모르는 동료가 된다.

이 결과는 홀로 선 것이 아니다. 경쟁하는 또 다른 추론 모델의 주장과 같은 시기에 겹친다. 그 모델은 이산기하학에서 약 80년 된 에르되시 추측을 반증했다고 전해졌고, 현역 수학자들이 다듬고 보증했다. 두 연구소, 두 방법, 하나는 형식적 검증에 기대고 다른 하나는 날것의 추론 사슬에 기대어, 몇 주 차이로 같은 최전선에 닿았다. 경쟁은 더 이상 똑똑해 보이는 챗봇의 문제가 아니다.

이 연구는 이번 달에 공개된 논문에 정리되었고, 방법은 열린 도구, 곧 Lean과 공동체가 쌓은 라이브러리에 기댄다. 그래서 외부 그룹은 기업 블로그를 믿는 대신 증명을 검사하고 다시 돌려볼 수 있다. 딥마인드는 이 시스템이 회사 밖 연구자에게 닿을지는 밝히지 않았다. 지켜볼 숫자는 아홉이 아니다. 그 2.5퍼센트가 10이 되고, 다시 20이 되느냐다. 그날이 오면, 이 기계들이 무엇을 위한 것인가라는 논쟁은 처음부터 다시 시작해야 한다.

관련 기사

마이크로소프트, Anthropic을 Maia 200의 첫 외부 고객으로 만들기 위한 협상

SpaceX 상장 신청서, Anthropic이 Colossus에 연 150억 달러를 지불 중임을 드러내다

OpenAI, 수학 전용 모델 없이 80년 묵은 기하학 문제를 풀다

Opus 4.6에 2점 뒤졌지만 5배 저렴, Gemini 3.5 Flash가 셈을 다시 쓴다