필즈상 수학자가 말하는 '수학의 버전 업'
테렌스 타오(Terence Tao)라는 이름은 개발자분들도 한 번쯤 들어보셨을 거예요. 필즈상을 받은 UCLA 수학자이고, '살아 있는 수학자 중 가장 똑똑한 사람'이라는 별명으로 불리는 분인데요. 이분이 칼텍(Caltech)에서 발표한 'Math 2.0' 슬라이드가 공개됐어요.
제목만 봐도 감이 오시죠? 소프트웨어처럼 수학도 1.0에서 2.0으로 넘어가고 있다는 이야기예요. Math 1.0은 우리가 아는 전통적인 수학이에요. 수학자 한 명이나 몇 명이 칠판과 종이로 증명을 쓰고, 논문을 내면 심사자가 몇 달씩 걸려 꼼꼼히 읽어보는 방식이죠. Math 2.0은 여기에 증명 보조기(proof assistant), AI, 대규모 협업이 더해진 새로운 작업 방식이고요.
재밌는 건 타오가 그리는 미래가 우리 개발자들한테 아주 익숙한 모습이라는 거예요. '수학의 깃허브화'라고 불러도 될 정도거든요.
핵심 도구: 증명을 컴파일하는 언어, Lean
Math 2.0의 한가운데에는 Lean이라는 도구가 있어요. 이게 뭐냐면, 수학 증명을 코드로 써두면 컴퓨터가 그 증명이 논리적으로 맞는지 한 줄씩 검사해주는 프로그래밍 언어예요.
개발자식으로 비유해볼게요. 타입스크립트에서 타입이 안 맞으면 컴파일 에러가 나잖아요? Lean에서는 '명제'가 타입이고, '증명'이 그 타입을 만족하는 값이에요. 그래서 증명에 논리적 빈틈이 있으면 컴파일이 안 돼요. 컴퓨터 과학에서는 이걸 커리-하워드 대응(Curry-Howard correspondence)이라고 부르는데, 쉽게 말해 '증명을 쓰는 일과 프로그램을 짜는 일은 사실 같은 일'이라는 아이디어예요.
이게 중요한 건 신뢰 문제를 풀어주기 때문이에요. 기존 방식으로는 100페이지짜리 증명이 맞는지 확인하려면 전문가가 몇 달, 길면 몇 년을 써야 했어요. Lean으로 작성된 증명은 컴퓨터가 몇 분이면 검증해요. 리뷰어가 모든 줄을 직접 읽지 않아도 되는 거죠.
이미 현실이 된 사례들
타오는 말로만 이러는 게 아니라 직접 해봤어요. 2023년 말에는 동료들과 함께 증명한 PFR(Polynomial Freiman–Ruzsa) 추측을 Lean으로 옮기는 프로젝트를 열었는데, 여러 기여자가 참여해서 3주쯤 만에 형식화(증명을 컴퓨터가 검사할 수 있는 형태로 옮기는 작업)를 마쳤어요.
더 인상적인 건 2024년에 시작한 방정식 이론 프로젝트(Equational Theories Project)예요. '마그마'라는 대수 구조에는 방정식 법칙이 약 4,700개 있는데, 그 사이에 '이 법칙이 성립하면 저 법칙도 성립하는가'를 전부 따져보는 작업이었어요. 확인할 경우의 수가 2,200만 개가 넘었으니 사람 혼자서는 평생 걸려도 못 끝낼 일이죠. 이걸 수십 명의 자원봉사자, 자동 정리 증명기, Lean 검증을 엮어서 끝냈어요.
이 프로젝트가 돌아간 방식은 오픈소스 개발 그 자체였어요. 큰 문제를 작은 이슈로 쪼개고, 각자 맡은 부분을 풀어서 올리면, Lean이 CI처럼 자동으로 검증해줬거든요. 기여자가 전체 그림을 다 알 필요도 없고 서로를 믿을 필요도 없었어요. 컴파일러가 대신 확인해주니까요.
AI는 어디에 들어갈까
여기에 AI가 붙으면서 판이 더 커지고 있어요. 구글 딥마인드의 AlphaProof는 국제수학올림피아드 문제를 Lean 증명으로 풀어냈고, 타오는 2025년에 딥마인드 연구진과 함께 AlphaEvolve라는 시스템으로 수십 개의 수학 문제를 탐색한 실험 결과도 공개했어요.
타오가 강조하는 건 'AI가 수학자를 대체한다'가 아니에요. AI는 그럴듯하지만 틀린 답을 자신 있게 내놓는 일이 많잖아요? 그래서 AI가 만든 증명을 Lean으로 검증하는 조합이 중요해요. AI는 아이디어를 대량으로 쏟아내고, Lean은 그중 진짜만 걸러내는 거죠. 그러면 수학자는 이 흐름을 설계하고 방향을 잡는 프로젝트 매니저나 아키텍트에 가까운 역할을 맡게 될 수 있다는 거예요.
개발자에게 왜 중요할까
'수학 얘기가 나랑 무슨 상관이야?' 싶으실 수도 있는데, 사실 개발자랑 꽤 가까운 이야기예요.
첫째, AI가 짠 코드를 어떻게 믿을 것인가는 지금 업계의 가장 큰 숙제예요. 수학계가 'AI + 형식 검증'으로 이 문제를 풀어가는 방식은 소프트웨어에도 그대로 가져올 수 있어요. 실제로 AWS는 권한 정책 언어 Cedar의 핵심 로직을 Lean으로 검증하고 있고, 형식 검증은 금융, 보안, 인프라 분야에서 이미 쓰이고 있어요.
둘째, Lean은 그 자체로 꽤 괜찮은 함수형 프로그래밍 언어예요. 하스켈이나 러스트의 타입 시스템을 좋아하신다면 Natural Number Game 같은 튜토리얼로 가볍게 시작해볼 만해요. 게임 스테이지를 깨듯 증명을 하나씩 풀어가는 방식이라 수학 전공이 아니어도 재밌게 할 수 있어요.
셋째, 협업의 패러다임이에요. 타오가 수학에서 실험하고 있는 '잘게 쪼개고, 자동으로 검증하고, 서로 믿지 않아도 협업하는' 구조는 우리가 매일 하는 일의 이상적인 모습이기도 해요. 테스트 커버리지가 높고 타입이 엄격한 코드베이스일수록 처음 온 기여자도 마음 놓고 PR을 올릴 수 있는 것과 같은 원리거든요.
마무리
한 줄로 정리하면, 수학은 지금 '천재 개인의 예술'에서 '검증 가능한 대규모 협업'으로 버전업하는 중이고, 그 도구와 문화는 소프트웨어 개발에서 빌려온 거예요.
여러분은 어떻게 보세요? AI가 짠 코드를 형식 검증으로 확인하는 날이 실무에도 올까요, 아니면 결국 테스트 코드면 충분할까요?
🔗 출처: Hacker News