최근 인공지능(AI)이 수학 분야에서 인간의 능력을 뛰어넘는 놀라운 성과를 보여주며 학계에 큰 파장을 일으키고 있습니다. 특히 AI가 수학적 난제에 대한 '반례(counterexample)'를 찾아내고, 복잡한 증명을 '형식화(formalization)'하는 데 성공하면서, 수학 연구의 패러다임이 근본적으로 변화할 조짐을 보이고 있습니다.
두 달 전, 챗GPT(ChatGPT)는 이산 기하학의 오랜 난제인 에르되시 단위 거리 추측(Erdős' Unit Distance conjecture)에 대한 반례를 제시하며 학계를 놀라게 했습니다. 이는 1960년대 골로드-샤파레비치 정리(Golod-Shafarevich theorem)라는 심오한 수론(number theory) 정리를 활용한 것으로, 초기에는 인간 수학자들의 검증을 거쳤습니다. 이후 튜링상 수상자 얀 르쿤(Yann LeCun)이 공동 설립한 로지컬 인텔리전스(Logical Intelligence)는 챗GPT가 생성한 논문 전체를 Lean이라는 형식 검증 시스템으로 자동 형식화(autoformalized)하는 데 성공했습니다. 더 나아가, 한 달 뒤에는 OpenAI의 보리스 알렉세예프(Boris Alexeev)가 새로운 모델 Sol을 활용해 에르되시 반례를 수학의 공리(axioms)만으로 완전하게 형식화하는 데 성공했습니다. Sol은 3주 만에 120만 줄의 Lean 코드를 생성했는데, 이는 Lean의 핵심 수학 라이브러리인 mathlib이 9년에 걸쳐 작성한 230만 줄의 절반에 달하는 엄청난 양입니다.
이러한 AI의 발전은 단순히 계산을 돕는 수준을 넘어, 새로운 수학적 발견과 증명 과정 자체를 혁신하고 있습니다. 특히 AI가 수십 년간 난제로 여겨져 온 전역 유체장 이론(global class field theory)과 같은 복잡한 개념을 형식화하는 데 기여하면서, 인간 수학자들이 접근하기 어려웠던 영역까지 탐색할 수 있는 가능성을 열었습니다. 이는 수학 연구의 속도를 가속화하고, 오류 없는 증명의 시대를 앞당길 것으로 기대됩니다. 앞으로 AI는 수학자들의 조력자를 넘어, 때로는 독립적인 연구 주체로서 수학의 지평을 넓히는 데 핵심적인 역할을 할 것입니다.