필즈상 수상자가 던진 도발적인 질문
테렌스 타오는 현존하는 가장 유명한 수학자 중 한 명이에요. 필즈상 수상자이면서, 최근 몇 년간은 수학계에서 AI와 형식 검증 도구를 가장 적극적으로 실험해 온 사람이기도 하죠. 그런 사람이 블로그에 '왜 아직 인간 수학자가 필요한가?'라는 제목의 글을 올렸어요. 제목만 보면 AI 회의론 같기도 하고, 반대로 항복 선언 같기도 한데요. 실제로는 그 어느 쪽도 아니에요. 지금 수학계가 어떤 상황이길래 이 질문이 나올 수밖에 없었는지, 그리고 이게 개발자인 우리와 무슨 상관인지 풀어볼게요.
배경: AI가 수학 올림피아드 금메달을 따는 시대
이 질문이 나온 배경부터 볼게요. 2024년에 구글 딥마인드의 AlphaProof가 국제수학올림피아드(IMO) 문제를 풀어 은메달 수준 점수를 냈고, 2025년에는 구글과 OpenAI의 모델이 자연어로 문제를 읽고 증명을 써서 금메달 기준을 넘겼어요. 올림피아드 문제는 '정답이 있는 닫힌 문제'라 실제 연구 수학과는 다르다는 지적도 있지만, 몇 년 전만 해도 상상하기 어려운 일이었죠.
여기에 Lean이라는 도구가 있어요. 이게 뭐냐면, 수학 증명을 컴퓨터가 한 줄 한 줄 기계적으로 검사할 수 있는 형태로 쓰게 해주는 '증명 보조기'예요. 개발자 입장에서는 타입 시스템이 아주 강력한 프로그래밍 언어라고 생각하면 돼요. 증명이 컴파일되면 논리적으로 맞다는 뜻이고, 컴파일이 안 되면 어딘가 구멍이 있다는 뜻이죠. AI가 만들어낸 증명이 맞는지 사람이 일일이 읽지 않아도 검증할 수 있는 길이 열린 거예요.
타오 본인이 이 조합을 실제로 써봤어요. 2023년에는 GPT-4를 연구 보조로 써본 경험을 공유했고, 2024년 가을부터는 수백 명이 참여하는 Equational Theories Project라는 협업 프로젝트를 이끌면서 4천 개가 넘는 등식들 사이의 관계 2천만 개 이상을 Lean으로 형식화하고, 그 대부분을 자동화 도구가 해결하게 했어요. 수학 연구를 마치 오픈소스 소프트웨어 개발처럼 '분업과 자동화'로 돌린 실험이었죠.
그래서 인간 수학자는 왜 필요한가
타오가 그동안 여러 인터뷰와 글에서 밝혀온 생각의 흐름을 따라가 보면, 답은 '문제를 푸는 것과 무엇을 풀지 정하는 것은 다르다'로 모여요.
첫째, 문제를 고르는 안목이에요. 수학에는 풀 수 있는 문제가 무한히 많지만, 그중 풀 가치가 있는 문제는 극소수예요. 어떤 정리가 다른 분야로 이어지는 다리가 될지, 어떤 방향이 막다른 길인지 판단하는 건 아직 사람의 몫이에요. AI가 아무리 증명을 잘 써도, 아무도 궁금해하지 않는 정리를 만 개 증명하는 건 의미가 없거든요.
둘째, 검증과 책임이에요. 타오는 예전부터 AI를 대학원생에 비유해 왔어요. 2023년에는 '평범하지만 아주 무능하진 않은 대학원생' 정도라고 했는데, 아이디어를 내는 건 학생이지만 그중 뭐가 진짜인지 걸러주는 건 지도교수의 몫이라는 뜻이었죠. Lean이 논리적 정확성은 검사해 주지만, 그 증명이 '원래 풀려던 문제를 제대로 형식화한 것인지'는 여전히 사람이 확인해야 해요. 문제 정의를 잘못하면 완벽하게 검증된 엉뚱한 답이 나오니까요.
셋째, 이해예요. 증명이 존재한다는 것과 왜 그런지 이해하는 건 달라요. 1976년 4색 정리가 컴퓨터로 증명됐을 때 수학자들이 불편해했던 이유도 이거였어요. 맞다는 건 알겠는데, 왜 맞는지 사람이 파악할 수 없었거든요. AI가 내놓는 증명이 늘어날수록 그걸 사람이 소화할 수 있는 형태로 재구성하는 일의 가치는 오히려 올라가요.
이걸 한 줄로 요약하면, AI는 수학의 '생산성'을 바꾸지만 수학의 '방향'을 정하는 일은 여전히 사람에게 남아 있다는 거예요. 타오는 이걸 부정적으로 보지 않아요. 오히려 한 명이 하나의 문제를 몇 년씩 붙잡던 방식에서, 여러 문제를 동시에 탐색하는 방식으로 수학이 바뀔 수 있다고 기대하는 쪽이에요.
개발자에게는 이미 익숙한 질문
이 논쟁, 어디서 많이 본 것 같지 않나요? 'AI가 코드를 짜는데 개발자가 왜 필요한가'와 구조가 똑같아요. 코딩 에이전트가 함수를 잘 짜는 것과, 어떤 기능을 만들어야 하는지 정하고, 잘못된 요구사항을 걸러내고, 결과물에 책임지는 것은 다른 일이거든요.
수학계의 Lean에 해당하는 게 우리에게는 테스트, 타입 시스템, CI예요. AI가 코드를 많이 낼수록 '이게 맞는지 기계적으로 확인하는 장치'의 가치가 올라가는 구조가 똑같죠. 그리고 '문제 정의를 잘못하면 완벽하게 검증된 엉뚱한 답이 나온다'는 교훈은, 요구사항을 잘못 이해한 채 테스트까지 통과시킨 코드를 한 번이라도 본 사람이라면 바로 공감할 거예요.
한국 개발자에게 주는 시사점
실무적으로 가져갈 게 세 가지 있어요. 첫째, AI 도구를 쓸 때 '무엇을 시킬지'를 정하는 능력에 투자하세요. 프롬프트 기술보다 문제 정의 능력이 더 오래가는 자산이에요. 둘째, 검증 인프라를 먼저 갖추세요. 타오가 Lean 없이 AI 증명을 신뢰하지 않듯이, 테스트와 타입이 없는 코드베이스에 AI를 들이는 건 위험해요. 셋째, Lean 자체도 한 번 만져볼 만해요. 함수형 프로그래밍과 의존 타입을 배우는 좋은 경로이고, AI와 형식 검증의 결합은 앞으로 소프트웨어 검증 분야로도 넘어올 가능성이 높거든요.
정리하며
핵심 한 줄: AI는 증명을 쓰는 속도를 바꾸고 있지만, 어떤 문제가 풀 가치가 있는지 고르고, 결과를 이해하고, 책임지는 일은 아직 사람에게 남아 있어요.
여러분은 어떻게 생각하세요? 개발 현장에서 '문제를 고르는 능력'이 정말 마지막까지 사람 몫으로 남을까요? 아니면 그것마저 몇 년 안에 AI가 더 잘하게 될까요? 그리고 여러분 팀에는 AI가 만든 결과물을 걸러줄 'Lean'에 해당하는 장치가 있는지도 궁금해요.
🔗 출처: Hacker News