필즈상 수상자이자 세계적 수학자 테렌스 타오가 AI와 형식 검증 도구가 수학 연구에 역사상 처음으로 분업 체계를 도입할 가능성이 있다고 주장했다. 타오에 따르면 수학은 다른 자연과학이나 산업 분야와 달리 문제 설정, 전략 수립, 실행, 결과 검증, 논문 작성 모두를 단 한 명의 연구자가 처리해야 하는 구조였다. AI와 형식 검증 시스템이 이 구조를 변화시킬 수 있다는 것이 그의 분석이다.
타오는 AI가 협업의 빈틈을 채우는 역할을 맡을 수 있다고 보면서도, 전략 생성과 검증이 동시에 고도화되지 않으면 오히려 검증되지 않은 아이디어만 범람하는 역효과가 날 수 있다고 경고했다. 그는 “자동화와 AI를 유익하게 활용할 수 있는 수준은 검증의 엄격함에 비례한다”고 밝혔다. 이는 수학처럼 증명이 절대 기준인 분야에서야 AI 활용의 효용이 극대화된다는 의미다. 현재 AI의 수학적 추론 능력은 분야별로 편차가 크며, 타오는 인간 연구자가 이 불균등함을 보완하는 역할에서 여전히 필수적이라고 강조했다.
타오가 제시하는 미래상은 ‘산업형 수학(industrial mathematics)’에 가깝다. 소수의 연구자가 수년간 홀로 난제를 파고드는 고전적 방식 대신, AI가 대규모 데이터를 처리하는 동안 인간은 수십 개의 관찰에서 ‘영감에 의한 추측’을 내놓는 형태의 대규모 협업 체제다. 이 구조에서는 각 참여자가 문제의 일부에만 특화할 수 있어 물리학이나 생명과학에서 오래전부터 자리잡은 분업 모델이 수학에도 처음으로 적용된다는 것이다.
수학 분야의 AI 활용은 최근 빠르게 확장되고 있다. 구글 딥마인드의 AlphaProof는 2024년 국제수학올림피아드(IMO) 문제 가운데 일부를 AI가 증명하는 성과를 보였고, 형식 증명 보조 도구인 Lean을 연구에 활용하는 수학자도 늘고 있다. 타오 역시 자신의 연구에 AI와 형식 검증 도구를 결합하는 실험을 이어가고 있다. 검증 인프라가 AI의 수학적 활용 한계를 결정짓는 핵심 변수라는 그의 시각은 향후 AI-수학자 협력 생태계의 방향을 가늠하는 중요한 기준점이 될 전망이다.
