구글 딥마인드 AI, 에르되시 미해결 문제 9개 증명

구글 딥마인드가 아직 풀리지 않은 수학 문제의 증명을 찾는 연구용 시스템 AlphaProof Nexus를 공개했다. 연구진은 수학자 에르되시가 남긴 미해결 문제 9개를 증명했다고 밝혔다. 정수 수열을 모아 둔 데이터베이스 OEIS에 올라 있던 미해결 추측 44개도 증명했다. 논문은 2026년 5월 미리 공개됐고, 10월 8일(현지시간) 다른 연구자들의 심사를 거쳐 학술지 Science에 실렸다.

어떤 문제를 풀었나

오랫동안 답이 나오지 않던 문제가 포함됐다. 연구진에 따르면 해결한 에르되시 문제 9개 중 2개는 56년간 미해결 상태였다. 연구진은 대수기하학의 질문도 해결했고, 최적화 분야에서는 기존에 알려진 한계를 개선했다고 밝혔다. 수학 경시대회 문제를 넘어 실제 연구 문제에 도전한 결과다.

성공한 문제는 도전한 전체 문제의 일부다. 에르되시 문제는 353개 가운데 9개를 풀었고, 344개는 풀지 못했다. OEIS 추측은 492개 가운데 44개를 증명했고, 448개는 해결하지 못했다. 실패한 시도에서는 핵심 증명 단계를 비워 두거나, 존재하지도 않는 정리를 근거로 삼은 사례가 나왔다.

AI가 쓴 증명, 맞는지 어떻게 확인하나

AlphaProof Nexus는 AI가 증명을 쓰고 검사 결과에 따라 고치는 과정을 반복한다. 연구자가 증명할 명제를 Lean이라는 증명 검사 도구의 언어로 입력하면 작업이 시작된다. 그러면 Gemini 3.1 Pro를 바탕으로 스스로 일을 처리하는 AI(에이전트)가 증명을 작성한다. Lean이 그 증명을 검사하고, AI는 결과를 받아 다시 쓴다.

출처: 구글 (보도자료)

규모를 키운 구성에서는 여러 시도를 서로 공유하며 풀이를 찾고, 일부 작은 문제는 AlphaProof에 맡긴다. AlphaProof는 Lean에서 증명을 찾도록 학습한 이전 시스템으로, 2024년 국제수학올림피아드 문제 풀이에 쓰였다. 이번 연구는 그 도구를 필요할 때만 부르면서, 언어모델이 증명을 쓰고 검사를 반복하는 방식을 합쳤다.

Lean은 증명 과정의 논리가 맞는지만 검사한다. 입력한 명제가 원래 풀려던 수학 문제와 같은 뜻인지는 사람이 따로 확인해야 한다.

지금 직접 볼 수 있는 것

공개 저장소에 연구 결과가 올라와 있다. AI가 만들어 낸 Lean 증명과 사람이 쓴 일부 설명, 도전한 문제 목록을 볼 수 있다. 논문에 따르면 AI가 증명을 만들어 내는 데 든 비용은 문제 하나당 수백 달러 수준이다.

이번 연구는 AI가 수학 연구에 참여하는 방식을 구체적으로 보여줬다. 증명을 쓰고 검사 결과로 고치는 작업을 반복해 실제 미해결 문제에서 성과를 냈다. 앞으로는 더 다양한 문제에서도 성과가 이어지는지, 잘못된 증명을 얼마나 줄일 수 있는지가 관심사다.