테렌스 타오, AI가 수학 연구에 혁신을 가져올 수 있다고 주장

테렌스 타오가 말하는 변화의 핵심은 형식 검증(formal verification)과 AI 보조 증명 시스템의 결합이다. Lean이나 Coq 같은 증명 보조 도구는 수학적 논증의 각 단계를 기계가 검증 가능한 형태로 강제하는데, 여기에 거대 언어모델을 붙이면 증명 초안 생성, 보조정리(lemma) 탐색, 반례 검색 같은 작업을 자동화할 수 있다. 기존 수학 연구는 문제 정의부터 증명 전략 수립, 세부 계산, 최종 검증까지 한 명의 연구자가 전 과정을 머릿속에 쥐고 있어야 했다. 타오가 "역사상 처음으로 분업이 가능해진다"고 말하는 이유는, 형식화된 증명 환경이 작업을 모듈 단위로 쪼개고 각 모듈을 독립적으로 검증할 수 있게 만들기 때문이다. 즉 한 사람이 큰 그림을 잡고, AI와 다른 연구자들이 검증 가능한 하위 문제들을 병렬로 처리하는 "산업적 수학(industrial mathematics)" 구조가 성립한다.

이 구조는 소프트웨어 엔지니어에게 익숙한 패턴 — 인터페이스 정의, 모듈 분리, 자동화된 테스트, 병렬 협업 — 을 수학 연구에 그대로 이식한 것이다. 형식 검증은 본질적으로 타입 체커나 컴파일러와 같은 역할을 한다. 증명의 각 단계가 "컴파일"을 통과해야 하므로, 여러 사람이 합의된 인터페이스(정리의 시그니처) 위에서 내부 구현을 따로 채워 넣어도 전체 정합성이 깨지지 않는다. 엔지니어 관점에서 이는 모노리식하게 한 사람이 들고 있던 지식을 명세(spec)와 계약(contract) 기반 협업으로 전환하는 것과 동일하며, AI는 그 명세를 만족하는 코드(증명)를 생성하고 검증기는 CI처럼 정확성을 보증한다. 다만 타오가 강조하듯 인간은 "영감에 찬 추측(inspired guesses)" — 어떤 방향이 유망한지, 어떤 추상화가 옳은지 판단하는 설계 역할 — 에서 여전히 대체 불가능하다는 점도 우리 직무의 미래와 직결된다.

개발자 입장에서 주목할 실용적 함의는, 이것이 단순히 수학계 이야기가 아니라 형식 검증 + LLM 조합이 검증 가능한 소프트웨어 개발로 번질 신호라는 점이다. 스펙 기반 코드 생성, 형식 명세 위에서의 AI 페어 프로그래밍, 검증기가 보증하는 자동 리팩터링 같은 워크플로가 현실화되고 있으며, 타오가 묘사하는 "분업 모델"은 곧 AI 에이전트와 인간 엔지니어가 명세를 공유하며 협업하는 팀 구조의 청사진이기도 하다. 핵심은 AI가 코드를 쏟아내는 양이 아니라, 그 출력을 기계적으로 검증할 수 있는 경계(타입 시스템, 테스트, 형식 명세)를 얼마나 잘 설계하느냐에 생산성이 좌우된다는 것이다.

따라서 지금 준비해야 할 것은 두 가지다. 첫째, Lean/Coq 같은 형식 도구까지는 아니더라도 강타입 시스템, 속성 기반 테스트(property-based testing), 명확한 인터페이스 계약을 통해 "AI가 채워 넣고 기계가 검증하는" 구조를 코드베이스에 정착시키는 일이다. AI 생성 코드가 늘어날수록 검증 가능한 경계의 가치가 기하급수적으로 커진다. 둘째, 타오가 말한 "영감에 찬 추측"에 해당하는 역량 — 문제를 어떻게 분해할지, 어떤 추상화가 올바른지, 어떤 방향이 막다른 길인지 판단하는 설계·아키텍처 감각 — 에 투자하는 것이다. 세부 구현과 검증이 자동화될수록 엔지니어의 차별점은 "무엇을 만들지, 어떻게 쪼갤지"를 결정하는 상위 판단으로 이동하기 때문이다.