수학 연구 결과를 컴퓨터가 검증 가능한 형태로 바꾸는 '형식화(formalization)' 작업에 인공지능(AI)이 활용되는 새로운 방법론이 제시되었습니다. 조셉 K. 밀러(Joseph K. Miller)는 수학자가 AI 시스템을 지휘하고, 이 과정을 전략 게임처럼 진행하여 복잡한 수학 논문을 린 4(Lean 4) 증명 보조 도구로 옮기는 실험을 수행했습니다. 이 접근 방식은 AI가 증명 작성의 실제 실행을 담당하고, 인간 수학자는 전체적인 방향 설정과 문제 해결에 집중하는 역할을 합니다.
이 연구는 블라소프 방정식(Vlasov equation)의 평균장 유도(mean-field derivation)에 대한 완전하고 공리적으로 깔끔한 형식화를 사례 연구로 삼았습니다. 목표는 LaTeX 문서에 있는 수학적 내용을 린(Lean) 코드로 변환하는 것이며, 모든 증명이 컴파일되고 린의 기초 공리(foundational axioms)에만 의존함을 기계적으로 확인하는 것이 게임의 승리 조건입니다. 인간 수학자는 정의의 범위 설정, 분해 유도, 라이브러리 부족 부분 해결 등 지휘자 역할을 수행했고, AI 에이전트는 실제 증명 코드를 작성했습니다. 이 협업을 통해 주요 정리들은 약 일주일 만에, 전체 개발은 약 한 달 만에 완료되었습니다.
이러한 AI 보조 형식화는 수학적 증명의 정확성을 높이고, 복잡한 이론을 기계적으로 검증할 수 있게 함으로써 수학 연구의 신뢰성을 강화할 수 있습니다. 특히, 이번 사례 연구에서 얻어진 최적 수송(optimal transport) 관련 수학적 도구들은 린의 수학 라이브러리(Mathlib)에 독립적인 계층으로 통합될 수 있음을 보여주며, 이는 일반 수학 라이브러리의 확장 가능성을 시사합니다. 이 방법론은 특정 AI 시스템에 얽매이지 않고, 향후 다양한 AI 도구와 함께 발전할 수 있는 유연한 프레임워크를 제공하여 수학 연구와 교육 방식에 장기적인 영향을 미칠 잠재력을 가지고 있습니다.