AI가 수학을 ‘풀었다’고 말하기 전에 봐야 할 것들

정리보다 중요한 건 이해라는 주장

• 글쓴이 David Bessis는 수학의 진짜 산출물이 ‘정리(theorem)’가 아니라 명료함과 이해라고 봄.

  • Bill Thurston의 말을 빌리면, 수학의 결과물은 정리 그 자체가 아니라 사람들이 더 선명하게 생각할 수 있게 만드는 것임.
  • 이 관점에서 보면 AI가 문제를 풀거나 증명을 생성하는 능력만으로 ‘수학을 해결했다’고 말하는 건 꽤 위험한 단순화임.

• 글쓴이는 자기 경험으로 이 얘기를 시작함. 가장 좋은 정리는 결국 논문으로 쓰지 못했고, 두 번째로 좋은 결과도 arXiv 프리프린트에 남긴 채 정식 출판하지 않았다고 함.

  • 흥미로운 건 그가 어려웠다고 말하는 부분이 ‘증명’이 아니었다는 점임.
  • 진짜 어려운 일은 정확한 정의와 개념 틀을 찾는 것이었고, 그 틀이 잡히면 정리는 거의 자연스럽게 따라왔다고 회고함.

• 이게 글 전체의 큰 축임. 수학 커뮤니티는 겉으로는 정리 증명에 보상을 줬지만, 실제 가치는 개념 만들기와 이해 확장에 있었다는 것.

  • G. H. Hardy식 분위기에서는 설명, 교육, 정의 만들기가 낮게 평가되고, 어려운 정리를 증명한 사람이 가장 큰 보상을 받음.
  • 하지만 Thurston, Terry Tao, Peter Scholze 같은 수학자들은 오래전부터 정의, 이해, 사고방식의 변화를 수학의 핵심으로 말해왔음.

AI for math가 건드린 취약점

• 문제는 AI가 이 오래된 보상 체계를 정면으로 때리기 시작했다는 점임.

  • 수학계는 ‘정리 증명’을 객관적 성과 지표로 써왔고, 큰 정리를 푸는 것이 개념적 혁신의 증거처럼 여겨졌음.
  • 그런데 AI가 정리 증명만 빠르게 자동화하면, 그 지표는 더 이상 인간 수학자의 가치 전체를 대표하지 못함.

• Geoff Hinton이 수학을 Go나 Chess처럼 ‘닫힌 규칙 시스템’으로 말한 대목이 글쓴이를 특히 불편하게 만듦.

  • Go와 Chess는 승자와 패자가 있는 유한한 완전정보 게임임.
  • 수학은 그런 게임이 아니라, 어떤 질문을 만들고 어떤 개념을 세우며 어떤 방식으로 세계를 이해할지 계속 바뀌는 활동이라는 게 글쓴이의 반박임.

• AI for math 스타트업들이 큰돈을 받는 이유도 이 프레임에서 설명됨.

  • 순수수학 시장 자체는 작지만, ‘DeepMind가 Go와 Chess를 풀었듯 우리가 수학을 풀겠다’는 투자 스토리는 엄청 강력함.
  • 글쓴이는 이 프레임이 대중과 투자자에게 너무 매혹적이라, 실제 수학의 가치가 왜곡될 위험이 크다고 봄.

First Proof가 보여준 것과 못 보여준 것

• First Proof 프로젝트는 고급 수학자 11명이 AI의 연구 수준 수학 문제 해결 능력을 보려고 만든 벤치마크임.
  • 첫 배치로 10개의 연구 수준 문제를 냈고, Google, OpenAI 등 여러 팀이 시도함.
  • Daniel Litt의 집계로는 여러 시도를 합치면 10문제 중 6~8개가 맞게 풀렸을 가능성이 있다고 함.

• AI 시스템들은 많은 쓰레기 답도 같이 뱉었음.

  • 틀린 해답이 Lean으로 형식화됐다고 주장하는 경우도 있었고, 좋은 모델과 스캐폴드조차 자기 출력이 헛소리인지 안정적으로 감지하지 못했다고 함.
  • 인간도 틀린 증명을 쓰긴 하지만, 보통은 주요 아이디어와 장애물이 보이고 고칠 방향이 있음. 글쓴이는 이 차이를 매우 중요하게 봄.

• First Proof 문제 자체도 ‘수학의 끝판왕’과는 거리가 있었다고 짚음.

  • 글쓴이에 따르면 첫 배치 문제들은 깊은 돌파구라기보다 정리 증명 중간에 나오는 기술적 보조정리(lemma)에 가까웠음.
  • 기술적으로는 현재 AI 수준을 재기 좋은 난이도였지만, 대중 헤드라인에서는 ‘세계 최고 수학자들이 낸 연구 문제 10개를 AI가 박살냈다’로 포장될 위험이 있음.

Lean, Mathlib, 그리고 20만 줄짜리 문제

• 자동 형식화(autoformalization)는 AI가 만든 증명을 Lean 같은 언어로 바꿔 기계 검증 가능하게 만드는 기술임.

  • 겉으로는 정답 검증 문제를 해결해줄 것처럼 보임.
  • 하지만 글쓴이는 ‘맞는 증명’과 ‘수학 커뮤니티가 이어 쓸 수 있는 증명’은 다르다고 말함.

• Math Inc가 Maryna Viazovska의 8차원·24차원 구 채우기(sphere packing) 결과를 Lean으로 형식화한 사건이 대표 사례로 나옴.

  • Viazovska의 결과는 2022년 Fields Medal로 이어진 최상급 수학 성과임.
  • Math Inc의 형식화는 인상적이었지만, Mathlib 커뮤니티에서는 200,000줄짜리 검증되지 않은 덩어리를 공용 지식의 마스터 브랜치에 넣을 수 없다는 반발이 나옴.

• 여기서 중요한 단어가 canonization임.

  • 일회성 증명을 일반적이고 재사용 가능하고 일관된 라이브러리 수학으로 바꾸는 과정임.
  • 소프트웨어로 치면 ‘어쨌든 돌아가는 코드’를 장기 유지보수 가능한 공용 API와 모듈로 바꾸는 일에 가까움.

• 글쓴이는 앞으로 형식 수학이 두 층으로 갈라질 수 있다고 봄.
  • 하나는 Mathlib처럼 인간이 이해하고 재사용할 수 있는 층임.
  • 다른 하나는 기계적으로는 참이지만 아무도 이해하지 못하는 거대한 증명 덩어리, 글쓴이 표현으로는 Mathslop에 가까운 층임.

AI가 잘하는 것과 아직 못하는 것

• 글쓴이는 AI가 수학에서 엄청난 발견을 할 가능성을 부정하지 않음.

  • 오히려 LLM은 수학 문헌 전체를 학습할 수 있고, 인간 수학자가 평생 읽는 논문은 전체의 0.1%도 안 될 수 있다고 봄.
  • 기존 문헌 속 연결고리를 찾아내는 데 AI가 매우 강력할 수 있다는 점도 인정함.

• 그는 이것을 Overhang이라고 부름.

  • 과거 수학자들이 만든 개념과 문제들 사이에 아직 발견되지 않은 연결, 즉 누적된 잠재 가치가 엄청나게 크다는 뜻임.
  • LLM은 기억력과 패턴 매칭으로 이 연결을 인간보다 빨리 캐낼 수 있음.

• 하지만 현재 AI는 동시에 초인간적이고 비인간적임.

  • 어떤 패턴 찾기와 조합에서는 인간보다 강하지만, 왜 그 방향이 의미 있는지 설명하고 새로운 개념 체계를 세우는 데는 아직 약함.
  • 그래서 문제 풀이 supremacy가 개념 형성 adequacy보다 먼저 올 수 있는데, 이걸 곧바로 ‘초지능’이라고 부르면 곤란하다는 주장임.

수학계가 해야 할 일

• 글쓴이는 수학계가 이제 정직하게 말해야 한다고 봄. 수학은 문제 풀이 생산 라인이 아니라 인간이 세계를 이해하는 방식 자체를 확장하는 활동이라는 점을 전면에 세워야 한다는 것.

  • 지금까지는 정리 증명이 객관적 평가 기준이라 편했지만, AI 시대에는 그 기준만으로는 수학자의 역할을 설명하기 어려움.
  • 특히 학생과 대중에게 ‘답을 얻는 것’과 ‘이해가 바뀌는 것’의 차이를 설명하지 못하면 수학 교육도 흔들릴 수 있음.

• 그는 자율주행 단계처럼 Mathematical Intelligence Scale 또는 Mathematical Automation Scale이 필요하다고 제안함.

  • 예를 들어 AI가 First Proof를 다 풀더라도 ‘수학을 해결했다’가 아니라 ‘수학 자동화 레벨 3에 도달했다’처럼 말하자는 것임.
  • 객관 벤치마크는 필요하지만, 문제 설정, 개념 만들기, 정리 체계화, 이해 가능성 같은 주관적이지만 핵심적인 능력을 같이 봐야 한다는 얘기임.

• 결론은 비관만은 아님. 글쓴이는 AI 없이 수학하는 것이 LaTeX 없이 수학하는 것처럼 상상하기 어려워질 거라고 봄.

  • 대신 협업 방식, 연구 산출물, 순수수학과 응용수학의 경계, 교육 방식은 크게 바뀔 가능성이 큼.
  • 수학이 사라지는 게 아니라, 인간이 무엇을 이해하고 왜 이해해야 하는지 더 노골적으로 묻게 되는 시기로 들어간다는 쪽에 가까움.

---

기술 맥락

• 이 글의 기술적 선택은 AI 수학 시스템을 ‘정답 생성기’로 볼지, ‘지식 축적 도구’로 볼지에 있어요. First Proof 같은 벤치마크는 정답 생성 능력을 재는 데는 유용하지만, 수학 커뮤니티가 실제로 이어 쓸 수 있는 개념과 라이브러리를 만드는 능력까지 재지는 못해요.

• Lean과 Mathlib가 중요한 이유는 여기서 나와요. Lean은 증명이 논리적으로 맞는지 확인해주지만, Mathlib는 그 증명을 다음 사람이 재사용할 수 있게 정리한 공용 기반이에요. 그래서 20만 줄짜리 형식 증명이 참이어도, 좋은 API와 추상화가 없으면 장기적으로는 빚이 될 수 있어요.

• 소프트웨어 개발로 비유하면 더 직관적이에요. 테스트가 전부 통과하는 코드와 팀이 5년 동안 유지보수할 수 있는 코드는 다르거든요. AI가 전자를 빠르게 만들 수 있어도, 후자를 만들려면 도메인 모델링, 이름 짓기, 모듈 경계, 리뷰 문화 같은 인간적인 설계 감각이 필요해요.

• 그래서 이 논쟁은 수학만의 얘기가 아니에요. AI 코딩 에이전트, 자동 리팩터링, 코드 생성 도구도 결국 같은 질문을 만나게 돼요. ‘맞는 결과’를 넘어 ‘조직이 이해하고 축적할 수 있는 결과’를 만들 수 있느냐가 진짜 제품 가치가 되는 거예요.