AI 인공지능과 수학의 만남: 에르되시 문제 #124, AI가 증명하다
AI가 수십 년간 풀리지 않았던 에르되시 문제 #124(Erdős Problem #124)를 증명했다는 소식이 수학계에 큰 파장을 일으키고 있습니다. 이 문제는 단순한 수학 퍼즐이 아니라 1996년 Burr, Erdős, Graham, Li 등 저명 수학자들이 남긴 난제입니다. 최근 Robinhood CEO가 창업한 수학 AI 스타트업 Harmonic의 모델 'Aristotle'이 이를 해결하면서, AI의 수학 연구 진출이 어디까지 왔는지 많은 이들의 이목이 쏠리고 있죠.
이번 글에서는 에르되시 문제 #124의 정체, AI의 증명 방식, 그리고 수학계와 AI 업계의 반응을 쉽고 흥미롭게 정리해 드립니다.
에르되시 문제 #124란 무엇인가?
에르되시 문제 #124는 한마디로 "모든 충분히 큰 정수를 특수한 방식의 합으로 표현할 수 있는가?"에 관한 문제입니다.
구체적으로, 주어진 조건을 만족하는 정수 집합을 만들고 그 집합에다 "서로 다른 거듭제곱의 합"만을 사용해서 임의의 큰 정수를 표현할 수 있는지를 묻습니다.
핵심 조건은 다음과 같습니다:
여러 정수 $d_i$가 있을 때, $sum 1/(d_i-1) geq 1$이어야 함.
각 항은 $d_i$의 거듭제곱 꼴(예: $2^k$, $3^m$ 등).
이들을 조합해 충분히 큰 모든 정수를 표현할 수 있어야 함.
이 문제는 1996년 제기된 이후, 일부 집합(예: ${3,4,7}$)에 대해서만 성립함이 증명됐고 일반적인 경우는 미해결 상태였습니다.
AI Aristotle, 어떻게 문제를 풀었을까?
수학 AI인 Aristotle은 문제의 공식적인 명제(정의와 조건)만 받아들이고, 인간의 추가적 통찰 없이 '정형화된 증명'을 시도했습니다. 특별한 점은 세 가지 버전을 각각 증명했고, 이 중 가장 강력한 명제가 공식화되었죠.
Aristotle은 완전히 기계적으로 Lean(수학 증명 검증 시스템)을 통해 문제를 해석·변환했고, 검증 가능한 형식적 증명을 6시간 만에 완성했습니다. Lean은 이 증명을 1분 만에 체크해서 '명백히 맞다'는 결과를 냈죠.
그 과정에서 AI가 실수한 부분(조건 오기 등)을 스스로 수정, 명제를 더 강하게 만들기도 했습니다. 이는 사람 연구자와 유사한 '시행착오-수정-강화' 패턴을 보여줍니다.
“쉬운 문제였나?” 논쟁
AI의 증명을 본 수학자들은 약간 복잡한 감정을 내비쳤습니다. 일부는 "사실 올림피아드(수학경시) 수준의 간단한 증명이었고, 왜 그동안 인간들이 못 풀었는지 신기하다"고 평가했습니다. Thomas Bloom은 "정식으로 문제를 제기한 논문에서 요구한 더 어려운 버전은 여전히 미해결"이라며, 실제 증명한 버전이 원래 명제와는 다소 차이가 있음을 지적하기도 했죠.
실제 AI가 해결한 것은 '더 쉬운 변형 문제'였던 것으로, 문제 정의상의 작은 차이(초항 처리, 최대공약수 조건 등)가 난이도를 크게 바꾸었기 때문입니다.
AI, 정말 수학 문제를 ‘독립적으로’ 풀었나?
Harmonic 측은 "AI가 훈련 데이터로 이미 풀린 문제를 본 것 아니냐"는 의심이 나올 수 있다는 점을 인정했습니다. 하지만 Aristotele가 자연어로 된 수학적 설명만을 주고, 인간의 참고 없이 오로지 기계 학습과 증명 검증을 반복하며 풀어나간 과정은 매우 인상적입니다.
게다가, 실제로는 기존 논문들에도 1이 포함된 더 쉬운 형태의 문제에 대한 해법이 있었음이 뒤늦게 드러났지만, AI가 스스로 증명을 formalize(형식화)하고 Lean을 통해 검증했다는 점에 전문가들도 박수를 보내고 있습니다.
AI가 수학 연구 현장에 던지는 변화
이 현장은 기계가 인간 수학자들처럼 문제를 이해하고, 명제를 강화하며, 쉽고 간결한 증명을 찾아낼 수 있음을 보여준 첫 사례 중 하나입니다. 기존에는 AI가 국제수학올림피아드 수준의 문제까지만 풀 수 있는 줄 알았는데, 이제는 오랫동안 풀리지 않았던 오픈 문제까지 손댈 수 있다는 걸 보여준 셈이죠.
이 업적이 완벽히 검증되어 학계의 인정까지 받는다면, 앞으로 수학 연구의 방식이 변화하고, 더욱 복잡하고 실제적인 응용 문제에 AI가 활용될 날도 머지않아 보입니다.
남은 과제와 기대
아직 '원본 논문에서 제기한 더 어려운 문제'는 미해결 상태. AI와 인간이 협업하면 더 강력한 문제들도 풀릴 수 있을까?
“쉬운 문제”였다고 하지만, 그간 수많은 사람들이 간과했던 해법을 AI가 빠르게 찾아낸 건 충분히 대단한 일이죠.
Lean 등 형식적 검증 기술과 자연어 처리 모델의 결합이 진정한 AI 수학 연구의 길임을 보여줍니다.
요약과 실용적 조언
AI는 이제 단순 암산이나 문제풀이 단계를 넘어, 인간이 실수하는 부분이나 놓치고 있었던 논리 구조까지 스스로 분석하고 증명합니다. 앞으로 실세계에서 복잡한 최적화나 설계, 생명과학 등의 분야에도 이런 'AI적 사고-검증'의 장점이 확대될 것입니다.
수학적 난제나 복잡한 문제에 도전할 때, 인간의 직관과 AI 증명 도구를 병행하는 전략이 연구자들에게 가장 강력한 무기가 될 날이 머지않았습니다.
참고
[1] AI just proved Erdos Problem #124 | Hacker News - Hacker News
[2] Robinhood CEO Vlad Tenev’s Math AI Startup Claims To Have Solved An Erdos Problem That Was Open For 30 Years - OfficeChai
[3] Erdős Problem #124 공식 페이지 - Erdős Problems Forum