최근 인공지능(AI)이 수학 분야에서 인간의 오랜 난제를 해결하는 데 중요한 진전을 보였습니다. ChatGPT와 Claude 계열의 대규모 언어모델(LLM)들이 불과 몇 주 만에 에르되시(Erdős)의 단위 거리 추측, 그로텐디크(Grothendieck)의 군 스킴 질문, 야코비안(Jacobian) 추측 등 수십 년에서 100년 가까이 풀리지 않던 문제들의 반례(counterexample)를 찾아냈습니다. 이 중 일부는 Lean이라는 형식 검증 시스템으로 기계적 검증까지 완료되어, AI가 수학 연구의 핵심 단계인 반례 발견에서 인간을 추월하기 시작했음을 보여줍니다.
가장 주목할 만한 사례는 OpenAI의 새로운 모델 Sol입니다. Sol은 에르되시의 단위 거리 추측에 대한 반례와 이를 뒷받침하는 전역 유체론(global class field theory) 결과를 3주 만에 120만 줄의 Lean 코드로 형식화했습니다. 이는 지난 9년간 인간 수학자들이 작성한 mathlib 라이브러리 전체 코드의 절반에 달하는 엄청난 양입니다. 또한, Sol은 60년 된 그로텐디크의 군 스킴 질문에 대한 12쪽짜리 반례를 찾아냈고, Claude Fable은 이를 4시간 만에 1,076줄의 Lean 코드로 자동 형식화했습니다. 이 반례는 위수(order) 4이지만 4에 의해 소멸하지 않는 군 스킴의 존재를 증명하며, 기존 수학계의 통념을 뒤집는 결과였습니다. 이처럼 AI는 방대한 양의 코드를 빠르게 생성하고 복잡한 수학적 논증을 형식화하는 데 탁월한 능력을 보여주고 있습니다.
이러한 AI의 발전은 수학 연구의 패러다임을 변화시킬 잠재력을 가지고 있습니다. AI가 생성한 비형식적 수학을 그대로 신뢰할 수는 없지만, 추측을 Lean과 같은 형식 검증 시스템의 정확한 명제로 만들면 증명과 반증을 기계적으로 검사할 수 있게 됩니다. 이는 인간 수학자들이 잘못된 추측에 시간을 낭비하는 것을 막고, 검증된 반례를 통해 더 깊은 수학적 통찰을 얻는 데 집중할 수 있도록 돕습니다. 실제로 하버드 대학교(Harvard University)는 이미 모든 박사과정생, 박사후연구원, 교수에게 Fable 무료 접근권을 제공하고 있으며, 이는 AI 도구가 수학 연구의 필수적인 부분이 되고 있음을 시사합니다. AI는 더 이상 단순한 보조 도구가 아니라, 새로운 수학적 발견을 이끄는 핵심 주체로 부상하고 있습니다.