Terence Tao, AI 증명 풍요 시대 'Math 2.0' 제안... 인간 이해 중심 전환 촉구

증명 희소성에서 증명 풍요로

Terence Tao는 증명 희소성과 해법 찾기의 어려움이 특징인 Math 1.0에서, 현대 AI가 주도하는 증명 풍요의 Math 2.0 시대로의 전환을 제시한다. 이 변화는 수학의 세 가지 고유한 특성, 즉 객관적 검증 가능성(Lean 같은 도구로 컴퓨터가 증명 확인 가능), 디지털화 가능성(물리적 구현 불필요), 그리고 디지털 연구 문헌에서 확보 가능한 고품질 데이터에 의해 가능해진다.

무분별한 AI 사용의 위험

AI가 많은 미해결 문제를 풀 수 있게 되었지만, Tao는 문제 해결의 맹목적인 최적화가 이제 해당 분야에 적극적으로 해롭다고 경고한다. 과거에는 문제를 풀려는 노력이 가치 있는 통찰과 인간적 이해를 낳았다. 하지만 자동화된 도구를 통해 prematurely 해답에 도달하면 '가지 않은 길'의 탐구를 생략하여 주변 분야를 살균할 수 있다. 그는 인간의 이해를 높이는 정렬된(aligned) 해법과, 검증 과정의 약점을 악용할 수 있으나 기계적 통찰은 제공하지 않는 비정렬(misaligned) 해법을 구분한다.

새로운 지평과 실험 수학

Tao는 AI를 고립된 문제 해결이 아닌 실험 수학을 통해 연구 지평을 넓히는 데 사용해야 한다고 주장한다. 주요 사례는 다음과 같다:

• Equational Theories Project (2024–2025): 범용 대수에서 2,200만개 이상의 참/거짓 명제를 해결하기 위해 인간과 자동화된 논증을 크라우드소싱했다.
• Inverse Galois Problem challenge (2026): 가능한 25,000개의 Galois 군 각각에 대해 차수 24 다항식을 찾는 대회이며, 2단계에서는 차수 31까지 확장된다.
• Mathathon (11월 13-15일): 현재 증명이 불만족스러운 기존 결과에 대해 오픈소스 AI를 사용해 개선된 증명을 찾는 학생 주도 이벤트.
• Integrated Explicit Analytic Number Theory Network (IEANTN): 명시적 해석적 수론 분야의 상호 연결된 결과들을 담은 살아있는 '스프레드시트'.

향후 과제

Math 2.0 달성의 주요 병목은 기술이 아니라 상상력이다. Tao는 불투명한 증명에 대한 동기가 부여된 설명을 찾는 개방적 서술 문제에 집중하고, Mathlib 같은 대규모 형식 수학 라이브러리를 구축하며, 해석 가능성과 안전성을 위한 맞춤형 오픈소스 수학 모델을 개발할 것을 제안한다. 그는 문제를 풀려 시도하는 과정에서 얻는 교훈이 최종 해법 자체보다 종종 더 가치 있다고 강조한다.