How Terry Tao became an evangelist for AI in math

개요

천재 수학자 테렌스 타오(Terence Tao)는 AI와 컴퓨터 검증 시스템을 활용하여 대규모 협업을 통해 수학 연구 방식을 혁신하려는 선구적인 시도를 하고 있다.

주요 내용

• 초기 예측과 비전: 테렌스 타오는 2014년에 이미 수학자들이 수백 명과 함께 작업하고 컴퓨터가 논문 검증을 수행하는 미래를 예측했으며, 이는 당시에는 비현실적으로 여겨졌다.
• 공개 협업의 시작 (Polymath Project): 타오는 Timothy Gowers가 시작한 Polymath Project에 참여하여 대규모 수학 협업의 가능성을 확인했지만, 댓글 기반의 협업 방식과 검증의 어려움을 경험했다.
• 컴퓨터 검증 수학에 대한 관심: 타오는 오랜 기간 컴퓨터 검증 수학의 잠재력에 관심을 가져왔으며, 특히 Lean과 같은 증명 보조 시스템의 가능성을 인지하고 있었다.
• Lean과의 첫 경험: 2023년, 타오는 Kevin Buzzard의 권유로 Lean 시스템을 학습하기 시작했으며, 10페이지 분량의 짧은 증명을 Lean으로 구현하는 과정에서 비인간적인 부분의 공식화에 예상치 못한 어려움을 겪었음을 발견했다.
• PFR 추측의 Lean 형식화: 타오는 Ben Green, Timothy Gowers, Freddie Manners와 함께 증명한 다항식 Freiman-Ruzsa (PFR) 추측에 대한 논문을 Lean으로 형식화하는 프로젝트를 시작했다. 이 프로젝트는 대규모 협업을 통해 진행되었으며, 타오는 직접적인 코드 작성보다는 작업 조율에 집중했다.
• "Equational Theories" 프로젝트: 타오는 2024년에 "Equational Theories"라는 새로운 프로젝트를 발표하며, 4,694개의 대수적 법칙 간의 2,200만 개 논리적 함의를 Lean과 자동화된 정리 증명기를 사용하여 해결하는 대규모 실험을 시작했다.
• 새로운 수학 연구 패러다임: "Equational Theories" 프로젝트는 기존의 이론 중심 수학에서 벗어나, AI와 컴퓨터 검증을 결합한 "실험적" 수학의 새로운 시대를 열 가능성을 보여주었으며, 이는 CERN의 입자 가속기와 같은 대규모 과학 실험과 유사한 접근 방식이다.
• AI와 형식 검증의 결합: 타오는 LLM이 초보 연구자처럼 행동할 수 있지만, 복잡한 문제를 수많은 작은 하위 문제로 분해할 수 있다면 AI가 유용하게 활용될 수 있으며, Lean과 같은 형식 검증 시스템을 통해 AI 결과의 정확성을 보장할 수 있다고 주장한다.

시사점

테렌스 타오의 이러한 노력은 수학 연구의 효율성과 정확성을 높이고, AI와 인간 지능을 융합하여 기존에는 불가능했던 복잡한 문제 해결을 가능하게 하는 미래 수학의 새로운 지평을 열 것으로 기대된다.