필즈상 수상자가 내놓은 반대 방향의 예측
AI가 국제수학올림피아드(IMO)에서 금메달 수준의 성적을 내고, 수학 증명을 척척 써내는 시대가 됐어요. 그러면 자연스럽게 ‘이제 수학자는 필요 없어지는 거 아냐?’라는 질문이 나오죠. 그런데 현존 최고의 수학자 중 한 명으로 꼽히는 테렌스 타오(Terence Tao, UCLA 교수, 필즈상 수상자)가 블로그에 정반대 제목의 글을 올렸어요. We're gonna need a lot more mathematicians, 우리는 수학자가 훨씬 더 많이 필요해질 거라는 거예요.
타오는 AI를 멀리서 구경만 하는 사람이 아니에요. 최근 몇 년간 형식 증명 도구 Lean으로 직접 증명을 옮겨 보고, AI 도구를 연구에 써보고, 수많은 참여자와 자동화 도구가 함께하는 대규모 협업 프로젝트를 이끌어 온 사람이거든요. 그래서 이 주장은 막연한 낙관이라기보다 현장에서 나온 관찰에 가까워요.
핵심 논리: 싸지면 더 많이 쓰게 된다
이 주장을 이해하는 가장 쉬운 열쇠는 경제학의 제번스 역설이에요. 이게 뭐냐면, 어떤 자원을 쓰는 효율이 좋아지면 사용량이 줄어드는 게 아니라 오히려 늘어난다는 현상이에요. 증기기관이 석탄을 덜 쓰게 되자 석탄 소비가 오히려 폭증했던 게 대표적인 예죠.
수학에 대입해 보면 이래요. 지금까지 증명 하나를 만들려면 전문가가 몇 달, 몇 년을 매달려야 했어요. 그래서 ‘그만한 노력을 들일 가치가 있는 문제’만 다뤄졌죠. 그런데 AI가 증명의 상당 부분을 자동으로 만들어주면, 예전엔 너무 비싸서 손도 못 댔던 문제들이 갑자기 다룰 만한 문제가 돼요. 소프트웨어가 정말 올바르게 동작하는지에 대한 증명, 공학 시스템의 안전성 분석, 수천 개의 작은 보조정리를 체계적으로 쌓아 올리는 작업 같은 것들이요.
그럼 남는 질문은 누가 이걸 지휘하느냐예요. AI가 만든 증명이 정말 맞는지, 애초에 질문을 제대로 정의했는지, 결과가 무슨 의미인지 판단하는 건 여전히 사람의 몫이에요. 증명 생산량이 폭발하면, 그걸 설계하고 검토하고 해석할 사람도 그만큼 더 필요해지는 거죠.
이미 벌어지고 있는 변화
이게 먼 미래 이야기가 아니라는 신호는 곳곳에 있어요.
타오가 주도했던 Equational Theories Project가 좋은 예예요. 마그마라는 단순한 대수 구조에서 여러 등식 법칙 사이에 어떤 게 어떤 걸 함의하는지를 전수 조사한 프로젝트인데요, 확인해야 할 관계가 2천만 개를 넘었어요. 사람 혼자서는 절대 불가능한 규모지만, 자동 정리 증명기와 Lean, 그리고 많은 참여자가 역할을 나눠서 해냈어요. 여기서 사람은 증명을 하나하나 손으로 쓰는 대신 문제를 쪼개고, 도구를 연결하고, 자동화가 못 푸는 까다로운 사례를 붙잡는 역할을 했죠.
또 하나는 Lean 같은 형식 증명 언어의 부상이에요. 이게 뭐냐면, 수학 증명을 프로그래밍 코드처럼 작성해서 컴퓨터가 한 줄 한 줄 논리적으로 맞는지 검사하게 하는 도구예요. AI의 가장 큰 약점이 ‘그럴듯하지만 틀린 답’을 내놓는 건데, Lean으로 검증하면 이 약점을 상당 부분 메울 수 있어요. 대신 ‘정확히 무엇을 증명할지’를 형식 언어로 적는 일, 즉 명세(specification)를 쓰는 일이 새로운 병목이 돼요. 바로 여기가 수학적 훈련을 받은 사람이 필요한 지점이에요.
개발자에게도 낯선 이야기가 아니에요
사실 이 구조는 요즘 개발 현장과 똑같아요. AI 코딩 도구가 코드를 엄청나게 빨리 만들어주면서 코드 양은 늘었지만, 그 코드를 리뷰하고 설계 방향을 잡고 ‘이게 요구사항을 정말 만족하나’를 판단하는 사람의 가치는 오히려 올라갔잖아요. 수학에서 벌어지는 일이 소프트웨어에서도 거의 동시에 벌어지고 있는 셈이에요.
업계에서도 형식 검증은 조금씩 실무로 들어오고 있어요. AWS는 접근 정책 분석이나 인가 정책 언어 같은 영역에서 자동 추론 기법을 적극적으로 쓰고 있고, seL4 같은 운영체제 커널은 수학적으로 정확성이 증명된 사례로 유명하죠. AI가 증명 비용을 낮춰주면 이런 접근이 일부 고위험 시스템을 넘어 훨씬 넓은 영역으로 퍼질 가능성이 커요.
한국 개발자에게 주는 시사점
당장 전업 수학자가 되라는 이야기는 아니에요. 다만 몇 가지는 챙겨볼 만해요.
첫째, Lean 4를 한 번 만져보세요. Natural Number Game이라는 입문 튜토리얼은 게임처럼 가볍게 시작할 수 있어서 부담이 없어요. 함수형 프로그래밍 경험이 있다면 더 빨리 익숙해질 거예요.
둘째, 명세를 쓰는 능력을 키우세요. AI에게 일을 많이 맡길수록 ‘내가 정확히 무엇을 원하는지’를 모호함 없이 적는 능력이 핵심 경쟁력이 돼요. 이건 수학적 사고 훈련과 거의 같은 근육이에요.
셋째, 진로를 고민하는 분들이라면 수학을 ‘AI가 대체할 과목’으로 보기보다 AI를 지휘하는 데 필요한 언어로 보는 관점이 도움이 될 거예요.
마무리
한 줄 정리: AI가 증명을 싸게 만들수록, 무엇을 증명할지 정하고 그 결과를 이해할 사람의 가치는 올라간다.
여러분은 어떻게 보세요? AI 코딩 도구를 쓰면서 오히려 설계와 검증에 쓰는 시간이 늘었다고 느끼시나요, 아니면 결국 그 영역까지 AI가 가져갈 거라고 보시나요?
🔗 출처: Hacker News