수학 비전문가가 AI 에이전트와 형식 증명 시스템 린(Lean)을 이용해 50년 묵은 수학 난제인 콘웨이의 세분화 추측(Conway's refinement conjecture)을 증명하는 데 성공했습니다. 약 한 달간의 지난한 과정을 거쳐 기계적 검증을 통과한 증명을 얻어냈으며, 이는 AI가 복잡한 수학 연구에 기여할 수 있음을 보여주는 중요한 사례로 평가됩니다.
이 프로젝트는 수학 비전문가도 AI를 활용해 미해결 문제를 풀 수 있을지 시험하는 호기심에서 시작되었습니다. 초기에는 AI에게 논문을 주고 한 번에 증명을 맡기려 했으나, AI는 검증되지 않은 결과를 쌓거나 비표준 용어를 남발하며 반복적으로 실패했습니다. 돌파구는 기존 논문 형식화와 새로운 결과 형식화를 분리하고, 수학적 탐색과 린(Lean) 검증 작업을 몇 시간 간격으로 조정하는 데 있었습니다. 특히, AI 에이전트들을 PM, Math, Red, Lean 등으로 역할을 나누고, 검증되지 않은 결과 위에 새로운 결과를 쌓지 않도록 철저히 관리하는 것이 중요했습니다. 이 과정에서 약 400억 토큰, 현재 API 가격으로 약 4만 달러(한화 약 5천 5백만 원)에 달하는 컴퓨팅 비용이 소요된 것으로 추정됩니다.
콘웨이의 세분화 추측은 전능정수(omnific integers)에서 'ab = cd'이면 'a = ef, b = gh, c = eg, d = fh'를 만족하는 전능정수 e, f, g, h가 존재한다는 명제입니다. 이는 일반 정수에서 자연스러운 인수분해의 성질이 무한한 수를 포함하는 전능정수에서도 유지되는지를 묻는 문제입니다. 이번에 얻은 증명은 팔로마 레지스트리(Palomar registry)의 기계적 검증을 통과했으며, 린(Lean)과 해당 분야에 익숙한 일부 전문가들은 형식화된 명제가 올바른 것으로 보인다고 평가하고 있습니다. 하지만 아직 수학자들의 독립적인 검증은 받지 않은 상태로, 연구팀은 증명의 정확성을 확신하며 반박을 요청하고 있습니다.
이번 성과는 AI가 복잡한 수학적 추론과 증명 과정에 실질적으로 기여할 수 있음을 보여줍니다. 특히, 전문 지식이 부족한 사람도 AI의 도움을 받아 난제를 탐색하고 해결의 실마리를 찾을 수 있다는 점에서 의미가 큽니다. 하지만 동시에 AI의 결과물을 맹신하지 않고, 사람의 비판적인 검토와 체계적인 프로젝트 관리가 필수적임을 시사합니다. AI가 생성한 비표준 용어나 순환 논증을 걸러내고, 검증된 결과만을 기반으로 다음 단계를 진행하는 '인간-AI 협업'의 중요성을 강조하는 사례라 할 수 있습니다. 앞으로 AI가 수학 연구의 새로운 지평을 열 잠재력을 가지고 있지만, 그 과정에서 인간의 역할은 여전히 핵심적일 것입니다.