수학자들이 AI를 위한 자문 그룹을 만든 이유
테렌스 타오는 현존하는 수학자 중 가장 유명한 사람 중 하나인데요. 이 분이 최근 몇 년 동안 AI와 수학의 만남에 대해 가장 적극적으로 발언해 온 사람이기도 해요. 그 타오가 블로그에 '수학과 인공지능에 관한 자문 그룹'을 소개하는 글을 올렸어요. 글의 취지를 요약하면, AI가 수학 연구에 들어오는 속도가 너무 빨라서 수학계가 개인 차원이 아니라 조직 차원에서 방향을 고민할 때가 됐다는 거예요. 이 자문 그룹은 AI가 수학 연구, 교육, 출판에 미치는 영향을 살피고 수학 커뮤니티에 조언하는 역할을 맡게 될 것으로 보이는데요, 왜 지금 이런 조직이 필요해졌는지를 알려면 지난 2년 동안 무슨 일이 있었는지부터 봐야 해요.
2년 만에 달라진 풍경
2024년 여름, 구글 딥마인드의 AlphaProof가 국제수학올림피아드 문제를 풀어 은메달 수준 점수를 냈어요. 그때만 해도 '형식 언어로 번역해 주고 시간도 많이 줬으니 반칙 아니냐'는 반응이 있었죠. 그런데 2025년 여름에는 OpenAI와 딥마인드가 각각 자연어로 문제를 읽고 자연어로 증명을 써서 금메달 기준을 넘겼어요. 이건 이야기가 달라요. 사람이 푸는 방식 그대로 푼 거니까요.
동시에 다른 쪽에서는 '형식 검증'이 커지고 있어요. 이게 뭐냐면, 증명을 사람이 읽는 글이 아니라 컴퓨터가 한 줄 한 줄 검사할 수 있는 코드로 쓰는 거예요. Lean이라는 언어와 Mathlib이라는 거대한 수학 라이브러리가 그 중심에 있고요. 타오 본인이 2023년에 PFR 추측 증명을 Lean으로 형식화하는 프로젝트를 온라인으로 수십 명과 함께 3주 만에 끝냈고, 2024년에는 수천 개의 대수 방정식 사이 관계를 형식화하는 Equational Theories Project를 이끌었어요. 여기서 중요한 통찰이 나왔는데, 형식 검증이 있으면 '모르는 사람과도, 심지어 AI와도' 안심하고 협업할 수 있다는 거예요. 기여자가 낸 증명이 틀렸으면 컴파일이 안 되니까요. 사람이 일일이 검토하지 않아도 기계가 걸러주는 구조가 생긴 거죠.
그런데 문제도 같이 왔어요
좋은 일만 있었던 건 아니에요. 2025년 가을에는 OpenAI 관계자가 'GPT-5가 에르되시 미해결 문제 여러 개를 풀었다'고 발표했다가, 알고 보니 이미 논문에 답이 있던 문제를 문헌 검색으로 찾아낸 거였다는 게 밝혀져서 발언을 철회한 일이 있었어요. 타오가 그때 '문헌 검색도 대단히 유용하지만 새 수학을 한 것과는 다르다'고 정확히 짚어줬죠. 또 AI로 생성한 그럴듯하지만 틀린 증명이 arXiv나 저널에 쏟아지면서 심사자들의 부담이 급증하는 문제, AI가 만든 결과의 저자 표기 문제, 학생들이 AI에게 숙제를 맡기는 교육 문제까지 한꺼번에 터졌어요. 개별 수학자가 각자 판단하기엔 너무 큰 질문들이라, 커뮤니티 차원의 자문 조직이 필요해진 거예요. 타오는 이전부터 AI 능력을 과장하는 쪽과 무시하는 쪽 사이에서 '실제 능력을 정확히 측정하고 정직하게 보고하자'는 입장을 지켜왔는데, 이 그룹도 그 연장선에 있다고 보시면 돼요.
개발자 관점에서 왜 흥미롭냐면
이건 수학자들만의 얘기가 아니에요. 소프트웨어 업계가 지금 겪는 문제와 구조가 똑같거든요. AI가 짠 코드를 어떻게 검증할 것인가, AI 기여의 저자를 어떻게 표기할 것인가, AI 도구 벤치마크 점수를 어디까지 믿을 것인가. 수학계가 찾은 답 중 하나가 '형식 검증'이라는 점은 특히 눈여겨볼 만해요. 코드로 치면 타입 시스템과 테스트를 극단까지 밀어붙인 거니까요. AI가 아무리 그럴듯한 걸 만들어내도 검사기를 통과 못 하면 소용없다는 원칙은 CI 파이프라인 설계에도 그대로 적용돼요.
한국 개발자라면 두 가지를 챙겨볼 만해요. 첫째, Lean 4는 그냥 수학 도구가 아니라 함수형 프로그래밍 언어이기도 해서, 타입 이론과 증명 보조기를 배우고 싶다면 지금이 진입하기 좋은 시기예요. AI가 Lean 코드를 꽤 잘 짜기 때문에 혼자 공부하기도 예전보다 훨씬 수월해졌고요. 둘째, AI 관련 발표를 볼 때 '벤치마크가 뭐였고 누가 검증했는지'를 먼저 묻는 습관이에요. 에르되시 문제 해프닝은 그 질문을 안 했을 때 어떻게 되는지 보여준 사례거든요.
정리하면
AI는 이미 수학 연구의 도구가 됐고, 수학계는 이제 개인이 아니라 조직으로 대응하기 시작했어요. 핵심은 능력 과장도 무시도 아닌, 정확한 측정과 검증이에요.
여러분 팀에서는 AI가 짠 코드의 검증 기준을 따로 두고 있나요? '컴파일 통과'와 '테스트 통과' 너머의 기준이 필요하다고 느낀 적 있으신지 궁금해요.
🔗 출처: Hacker News