수학의 미래: 테렌스 타오가 말하는 형식화, AI, 그리고 협업적 발견

게시일: 2026년 1월 4일 | 원문 작성일: 2025년 12월 31일 | 연사: 테렌스 타오 | 원문 보기

• • •

전환점: 새로운 기술 우주와의 만남

과학의 역사에서 진보는 종종 분야의 궤적을 바꾸는 결정적인 순간들과 함께 오죠. 테렌스 타오에게 그런 순간은 그가 공동 주최한 기계 지원 증명 컨퍼런스에서 찾아왔어요. IPAM(순수 및 응용 수학 연구소)에서 열린 그 컨퍼런스에서, 그는 막 그 힘을 보여주기 시작한 도구들의 “흥미진진한 세계”를 만나게 됐죠.

이 기술 환경에는 SAT 솔버와 전문 소프트웨어 패키지, ChatGPT의 폭발적 등장, 그리고 가장 결정적으로 형식 증명 보조 도구인 Lean1까지 모든 것이 포함되어 있었어요.

진정한 패러다임 전환이 진행 중이라는 신호는 페터 숄체(Peter Schölze)의 “liquid tensor experiment”2에서 왔어요. 이 야심 찬 18개월 프로젝트는 하나의 주요 정리를 성공적으로 형식화했죠. 시간이 오래 걸린 것처럼 들릴 수 있지만, 수십 년이 걸리곤 했던 20세기 형식화 프로젝트들에 비하면 획기적인 발전이었어요. 이 가속화된 속도는 GitHub를 버전 관리에 사용하는 것처럼 소프트웨어 엔지니어링의 방법론을 채택한 직접적인 결과였죠.

이것이 미래라고 확신한 타오는 “말만 하지 말고 직접 해보기로” 결심했어요. 한 달을 Lean 학습에 투자했는데, 이 경험이 고되면서도 중독적이었다고 해요. 자신의 학부 분석학 교과서를 쓰던 것—모든 것을 처음부터 쌓아올리는—과 비교하기도 했고, 동료 수학자 케빈 버저드(Kevin Buzzard)가 “세계 최고의 컴퓨터 게임”이라고 부른 것을 플레이하는 것 같다고 표현했죠.

타오의 이 투자는 최근의 대형 언어 모델 발전으로 더욱 검증됐어요. 이제 이 모델들이 증명 단계들을 “자동 형식화”할 수 있게 되면서, 남은 지루한 작업마저 제거하고 완전히 새로운 가능성의 영역을 열어줄 거예요.

• • •

수학적 마음의 재구성: 형식화가 인지를 어떻게 향상시키는가

사상가가 사용하는 도구는 단순히 작업을 돕는 것이 아니라 인지 과정 자체를 근본적으로 재구성할 수 있어요. 타오에게 형식화는 단순히 증명을 검증하는 방법이 아니라 더 깊고 명확한 사고 방식을 달성하는 수단이죠. 형식화의 훈련은 그가 “비효율적인 사고 방식”이라고 부르는 것을 정리하면서 수학에 대한 그의 인지적 접근을 여러 가지 뚜렷한 방식으로 재편했어요.

• ”보이지 않는 가정”을 보이게 만들기 — 수학 논문들은 명시되지 않은 전제와 암묵적인 생략으로 가득 차 있어요. 형식화 과정은 이러한 가정을 드러내서, 모든 논리적 단계를 명시적으로 만들고 논증의 진정한 토대를 밝혀주죠.
• ”가장 깔끔한” 정의 발견 — Lean에서 비효율적인 정의는 사소한 보조정리조차 증명할 때 연쇄적인 어려움을 만들어요. 시스템이 서투른 정의를 “벌”하기 때문에, 가장 우아하고 효과적인 형식을 찾게 되고, 이는 궁극적으로 증명 전체 구조를 단순화해요.
• 도구의 “자연스러운 형태” 찾기 — Lean의 자동 “린터”는 완성된 증명을 분석해서 불필요한 가설을 식별할 수 있어요. 이 기능은 주요 발전으로 이어질 수 있죠. 타오가 지적하듯이, 특정 조건(예: 양수일 때만)에서만 쓸 수 있다고 생각했던 도구가 실제로는 더 일반적인 상황에서도 작동한다는 것이 드러날 수 있어요. 형식화는 이러한 가정들을 스트레스 테스트하여 수학적 도구의 진정한 “자연스러운 형태”를 밝혀줘요.

이러한 인지적 전환은 타오의 수학적 학습 3단계 프레임워크에 직접적으로 매핑돼요:

숨겨진 가정과 비효율성을 드러냄으로써, 형식화는 엄밀한 단계에서 사후-엄밀한 단계로 전환하려는 수학자들에게 강력한 보조 도구로 작용해요. 가정을 보고, 정의를 간소화하고, 도구의 “자연스러운 형태”를 찾는 이 새로 발견된 인지적 명확성은 단지 추상적인 이점이 아니에요—타오가 곧 실제로 경험하게 될 놀라운 효율성을 직접 가능하게 하죠.

• • •

“아하” 모먼트: 형식화된 증명의 실용적 힘

형식화의 인지적 이점은 심오하지만, 현역 수학자를 진정으로 빠져들게 만든 것은 놀라운 실용성의 순간들이에요. 타오가 형식화에 완전히 전환하게 된 건 이론 때문이 아니었어요—기존 방법에 비해 거의 믿을 수 없을 정도의 우월성을 보여준 두 가지 실제 경험, 바로 증명 수정과 협업에서의 경험 덕분이었죠.

첫 번째 “아하” 모먼트: 증명의 수정 가능성

타오의 첫 번째 “아하” 순간은 증명의 수정 가능성에 관한 것이었어요. Polynomial Freiman-Ruzsa(PFR) 추측을 형식화하는 동안—20명이 3주에 걸쳐 진행한 주요 작업—팀은 특정 상수 12로 증명을 확립했어요. 얼마 후, 상수를 11로 낮출 수 있는 경로를 제안하는 프리프린트가 등장했죠.

또 다른 3주의 작업이 필요할까 걱정하는 대신, 팀은 형식화된 증명의 최종 진술을 12에서 11로 간단히 변경해봤어요. 타오가 설명하듯이, “다섯 줄 정도가 빨갛게 변했어요.” 하지만 새 프리프린트의 아이디어로 그 줄들을 고칠 수 있었죠. 그런데 이것이 연쇄 반응을 일으켰어요: “그렇게 하니까 다른 10개의 줄이 또 빨갛게 변하더라고요.”

종이에서는 불가능했을 이 연쇄적, 반복적 디버깅 과정이 모든 의존성을 추적하고 만 줄짜리 전체 증명을 단 하루 만에 업데이트할 수 있게 해줬어요.

두 번째 “아하” 모먼트: 수학의 원자화

타오의 두 번째 경험은 수학의 모듈성과 원자화를 보여줬어요. 다른 프로젝트의 협력자가 거대한 증명의 한 문제 있는 줄에서 막혔죠. 타오는 전체 맥락을 이해할 필요 없이 관련된 세 줄만 검사하고, 구체적인 문제를 파악해서 그것을 고칠 “원자적 진단”을 제공할 수 있었어요.

이것은 “서로의 문장을 완성할 수 있는” 전문가들 사이의 깊고 공유된 이해를 필요로 하는 전통적 협업과 극명하게 대비돼요. 형식화는 그 정밀하고 자기 완결적인 진술로 고도로 표적화된 기여를 가능하게 하죠.

수학을 별개의, 검증 가능한 구성요소로 분해하는 이 능력은 이 분야를 소규모 그룹 작업의 한계를 넘어 완전히 새로운 대규모 협업 생태계로 나아갈 수 있게 해요.

• • •

새로운 협업: 스타 그래프에서 전문화된 생태계로

역사적으로 과학적 협업은 인간 의사소통에 의해 제약받아 왔어요. 타오의 경험은 중앙 집중식 프로젝트에서 디지털 기반 위에 구축된 탈중앙화되고 전문화된 생태계로 이동하는 분야 전체 진화의 축소판이에요.

옛 패러다임은 “우연한 연결”을 만들기 위해 수학 문제를 크라우드소싱하는 것을 목표로 한 Polymath 프로젝트3로 예시돼요. 성공적이긴 했지만, 치명적인 한계에 시달렸죠: 한 중심 인물이 모든 기여를 확인하고 요약하는 “병목” 역할을 해야 했어요. 타오가 설명하듯이 이 “스타 그래프” 모델은 “극도로 지치게 하는” 것이었고 확장되지 않았어요.

형식화와 AI는 이러한 한계를 극복하는 새로운 패러다임을 가능하게 해요:

이 모델의 핵심 특징들:

• 매끄러운 협업 — 서로 다른 스킬셋을 가진 기여자들이 효과적으로 함께 일할 수 있어요. 한 사람은 수학 도메인 전문가, 다른 사람은 Lean 전문가, 세 번째는 GitHub 전문가일 수 있죠. 모든 사람이 모든 것을 알 필요가 없어요.
• 역할 분담 — 모든 협력자가 모든 것을 하는 모델에서 전문화된 역할을 가진 모델로 전환해요. 이는 “혼자 일하는 해커”에서 프로젝트 매니저와 QA가 있는 기업 수준 팀으로의 소프트웨어 엔지니어링 진화를 반영하죠.
• ”수학자”의 정의 확장 — 이 전문화는 수학을 높은 수준에서 이해하는 프로젝트 매니저나 도메인 전문가가 아닌 형식화 전문가 같은 새로운 역할을 만들어내요.
• 진입 장벽 낮추기 — 문제를 더 작고 잘 정의된 작업으로 모듈화함으로써, 이 도구들은 “시민 수학자”에게 힘을 실어줄 수 있어요. 부분적인 스킬셋을 가진 개인들이 연구 수준의 수학에 의미 있게 기여할 수 있죠.

”스타 그래프”에서 전문화되고 모듈화된 생태계로의 이 진화는 단순한 사회적 조직의 문제가 아니에요—이전에는 상상할 수 없었던 규모의 프로젝트, 예를 들어 전체 수학 분야의 살아있는 동적 지도를 만드는 것과 같은 프로젝트를 수행하는 데 필요한 핵심 인프라예요.

• • •

구체적 비전: 분석적 정수론의 살아있는 지도 구축

자동화의 가장 강력한 응용은 인간이 이미 끌리는 유명한 문제를 다루는 것이 아니라, “인간이 좋아하는 것과 완전히 직교하는”4 지루한 작업을 처리하는 것이라고 타오는 주장해요. 분석적 정수론에 대한 그의 비전이 대표적인 예죠: 그가 이 분야 작업의 최소 70%를 차지한다고 추정하는 계산적 고된 작업을 체계적으로 제거하는 프로젝트예요.

핵심 문제는 많은 작업이 약간 호환되지 않는 가정을 가진 정리들을 연결하는 것을 포함한다는 거예요. 이 복잡성을 관리하기 위해, 수학자들은 “속임수”를 사용해요: 특정하고 계산하기 어려운 상수들을 일반적인 자리 표시자 “C”로 대체하는 거죠. 이것은 계산을 줄이지만 큰 대가가 따라요: 결과가 명시적이지 않다는 거예요. 정리가 무언가가 “충분히 큰” 숫자에 대해 참이라고 증명할 수 있지만 얼마나 큰지는 명시하지 않아요.

타오는 이것을 해결하기 위한 자동화된 파이프라인을 구상해요. 엑셀 스프레드시트에 비유하면, 그의 목표는 “전체 분야의 살아있는 동적 최신 상태”를 만드는 것이에요. 이 시스템에서, 연구자가 제타 함수에 대한 새롭고 더 날카로운 경계를 증명하면, 그것을 형식화된 생태계에 넣기만 하면 돼요. 시스템은 그러면 이 새로운 정보를 수백 개의 의존 정리를 통해 자동으로 전파하여 몇 분 안에 업데이트할 거예요—현재 전체 논문을 다시 쓰는 것을 요구하고 아마도 십 년에 한 번 일어나는 작업을요.

영향은 심오할 거예요. 현재 수학자들은 지저분한 계산으로 이어지는 연구 경로를 “무의식적으로” 피한다고 타오는 언급해요. 그 결과, “놓친 기회”의 비율이 “엄청나죠.” 이 모든 장애물을 “폭파”할 수 있는 도구를 제공함으로써, 이 비전은 진보를 가속화할 뿐만 아니라 수학자들이 기꺼이 묻는 질문의 유형을 근본적으로 바꿀 거예요.

• • •

결론: 새로운 신뢰의 기반 구축

테렌스 타오의 경험은 수학이 근본적으로 변화하고 있음을 보여줘요. 이 분야는 인간의 한계—계산의 고된 작업, 의사소통의 부담, 그리고 깨지기 쉬운 사회적 신뢰 관계—에 의해 병목이 되던 상태에서 현대 도구의 확장 가능하고, 검증 가능하며, 협업적인 힘으로 증강되는 상태로 이동하고 있어요.

이 변환의 핵심에는 신뢰라는 주제가 있어요. 현재 시스템은 저자의 명성에 크게 의존해요. 연구자는 저자를 신뢰하기 때문에 결과를 기반으로 구축하죠. 이 모델에는 한계가 있는데, 필즈상 수상자 블라디미르 보예보츠키(Vladimir Voevodsky)의 이야기가 그 예에요. 그는 자신의 획기적인 논문 중 하나에서 발표 10년 후에 치명적인 오류를 발견했는데—다른 누구도 발견하지 못한 실수였죠.

형식화된 수학 위에 구축된 미래는 이 사회적 신뢰를 암호학적 확실성으로 대체해요. 증명이 Lean에 의해 보장되면, 연구자들은 한 번도 만난 적 없는 사람들의 작업 위에 자신 있게 구축할 수 있어요. 이 “신뢰 보장”은 진보를 가로막던 장애물을 제거하고 분야를 훨씬 더 넓은 커뮤니티에 개방할 수 있죠.

즉각적인 미래는 기존 수학 문헌의 진정한 오류율을 발견하는 매혹적인 가능성을 품고 있어요. 더 중요한 것은, 그것이 어느 때보다 더 넓고 다양한 사상가 커뮤니티에 수학의 프론티어를 열어주겠다고 약속한다는 거예요—마침내 그들의 기술의 창조적 본질에 집중할 수 있게 해주는 도구로 그들에게 힘을 실어주면서요.