수학계 최고 권위상인 필즈상 수상자 연구팀이 2년 넘게 공개적으로 진행해 온 수학 증명 형식화 프로젝트를 AI가 단 5일 만에 완료했다. 형식화란 수학자가 작성한 증명을 컴퓨터가 논리적으로 검증할 수 있는 코드로 변환하는 작업으로, 논리적 오류나 누락된 가정을 기계 수준에서 잡아낼 수 있어 수학계에서 높은 가치를 지닌다. 이번 성과는 수학자들 사이에서 AI 발전 속도에 대한 경외와 우려를 동시에 불러일으키고 있다.
해당 프로젝트는 케플러 추측의 8차원·24차원 풀이로 필즈상을 받은 뱌조우스카 교수 연구팀이 2024년 3월에 시작했다. 코드와 작업 계획을 공개해 외부 수학자들도 참여할 수 있는 방식이었으며, 형식화 과정에서 나온 정리와 개념을 공개 수학 라이브러리 매스립(mathlib)에 축적하면서 연구자들이 증명을 직접 이해하도록 하는 것이 목적이었다. AI 사용도 허용됐으나 공개 협업을 통해 집단 지성으로 작업을 채워가는 방식을 추구했다. 그러나 결과적으로 AI가 인간 팀의 다년간 작업 분량을 닷새 만에 처리하면서 연구팀 내에서도 복잡한 반응이 나왔다.
프로젝트에 참여한 이시우 EPFL 박사후연구원은 AI가 “중요한 정리를 자동으로 형식화했다는 점에서 의미 있다”고 인정하면서도 “코드 품질이 낮아 매스립 기준에 맞추려면 수정이 필요하다”고 밝혔다. 그는 더 나아가 “전체를 AI가 자동으로 완성하면서 사람이 직접 증명을 배우는 기회를 잃는 측면이 있다”며 갑작스러운 완료 통보에 기분이 좋지 않았다고 전했다. 미국 코네티컷대 이규환 수학과 교수는 최근 AI의 수학 능력에 대해 “6개월 전만 해도 AI가 박사과정 1~2학년 학생을 데리고 일하는 것 같았는데 이제 졸업을 앞둔 박사과정생 수준까지 올라왔다”고 평가하며 머지않아 박사후연구원 수준에 도달할 수 있다고 전망했다.
수학계에서는 AI를 어떻게 활용하느냐에 따라 결과가 크게 달라진다는 점도 지적된다. 인천대 이승재 수학과 교수는 “증명의 오류를 잡아내거나 반례를 찾을 때 AI가 빠르다”면서도 “문제를 통째로 던지는 방식은 통하지 않고, 질문을 세분화해 되짚어가며 사용해야 의미 있는 결과가 나온다”고 강조했다. 이시우 박사후연구원은 “대부분의 수학자들이 AI가 논문으로 출판할 수 있는 수준의 결과를 곧 만들어낼 것이라는 점을 인지하고 있다”고 말하면서, 연구를 막 시작하는 학부생이나 대학원생은 연구 실적보다 연구 능력을 키우는 것이 중요하기 때문에 가능하면 스스로 먼저 도전하는 습관이 필요하다고 당부했다.
