AI가 수학의 미해결 문제를 풀기 시작했다 — 수학계에 일어나고 있는 조용한 혁명

수학자도 AI를 쓰는 시대

프로그래밍, 글쓰기, 이미지 생성... AI가 못하는 게 뭐가 있냐는 말이 나올 정도인데요, 수학만큼은 좀 다른 이야기였어요. 수학 문제를 푸는 건 단순히 패턴을 학습하는 것과 차원이 다르거든요. 논리적 추론의 긴 사슬을 따라가야 하고, 창의적인 발상으로 완전히 새로운 증명 경로를 찾아내야 하니까요.

그런데 Quanta Magazine의 최근 보도에 따르면, 이 상황이 빠르게 바뀌고 있다고 해요. AI가 이제 단순한 수학 계산이 아니라, 수학의 미해결 문제에 대한 새로운 증명을 찾아내거나, 수학자들이 미처 보지 못했던 패턴을 발견하는 수준에 도달하고 있다는 거예요. 수학이라는 학문 자체의 연구 방법이 변하고 있는 셈이에요.

구체적으로 무슨 일이 일어나고 있나

AI의 수학 활용은 크게 두 가지 방향에서 진행되고 있어요.

첫 번째는 형식 증명(Formal Proof) 보조예요. 이게 뭐냐면, 수학 증명을 자연어가 아니라 컴퓨터가 검증할 수 있는 형식 언어로 작성하는 걸 말해요. Lean이라는 프로그래밍 언어(정리 증명 보조기)가 대표적인데, 수학 명제를 Lean 코드로 작성하면 컴퓨터가 그 증명이 논리적으로 올바른지 자동으로 검증해줘요. 문제는 이 형식 증명을 작성하는 게 매우 까다롭고 시간이 많이 걸린다는 건데, AI가 이 과정을 도와주고 있어요. 수학자가 증명의 큰 방향을 잡으면, AI가 세부 단계를 채워 넣거나 형식화를 자동으로 해주는 식이에요.

Google DeepMind의 AlphaProof가 대표적인 사례인데요, 2024년 국제수학올림피아드(IMO) 문제 중 일부를 풀어내면서 큰 주목을 받았어요. 올림피아드 수준의 문제는 정형화된 풀이법이 아니라 창의적인 접근이 필요한데, AI가 이런 문제를 풀 수 있다는 건 단순 계산 능력을 넘어선 거예요.

두 번째는 패턴 발견과 추측 생성이에요. 수학 연구에서 중요한 첫 단계가 "이런 패턴이 있는 것 같은데?"라는 추측(conjecture)을 세우는 건데요, AI가 방대한 수학 데이터에서 사람이 놓치기 쉬운 패턴을 찾아서 새로운 추측을 제안할 수 있어요. DeepMind가 2021년에 발표한 연구에서 매듭 이론(knot theory)과 표현론(representation theory) 분야에서 AI가 발견한 패턴이 실제로 새로운 정리로 이어진 사례가 있었어요.

이게 개발자와 무슨 상관인가요

"나는 수학자가 아닌데 이게 왜 중요하지?"라고 생각할 수 있는데요, 사실 소프트웨어 개발과 직접적으로 연결되는 부분이 있어요.

우선 형식 검증(Formal Verification) 분야가 있어요. 수학 증명을 검증하는 것과 소프트웨어의 정확성을 검증하는 것은 근본적으로 같은 문제예요. AI가 수학 증명을 자동화하는 기술이 발전하면, 소프트웨어 버그를 자동으로 찾아내거나, 코드가 명세대로 동작하는지 증명하는 도구도 함께 발전해요. 항공, 우주, 금융 같은 분야에서 소프트웨어의 무결성이 생명이나 돈과 직결되는 곳에서 이미 형식 검증을 쓰고 있는데, AI 덕분에 이게 더 보편화될 수 있어요.

또한 AI 추론 능력의 바로미터라는 관점도 있어요. 수학 문제 풀이는 AI의 논리적 추론 능력을 측정하는 가장 엄격한 벤치마크예요. 여기서 발전이 일어나면, 코드 생성, 디버깅, 아키텍처 설계 같은 소프트웨어 엔지니어링 영역에서도 AI가 더 정확한 추론을 할 수 있게 된다는 의미예요. 최근 Claude, GPT 같은 모델들의 코딩 능력이 빠르게 좋아지는 것도 이 추론 능력 발전과 궤를 같이 하거든요.

Lean과 형식 증명 생태계

개발자 관점에서 특히 흥미로운 건 Lean 4 생태계예요. Lean은 프로그래밍 언어이면서 동시에 정리 증명 도구인데, 문법이 Haskell이나 Rust와 비슷한 면이 있어서 프로그래머가 접근하기에 생각보다 장벽이 낮아요. 최근 수학 커뮤니티에서 Lean으로 작성된 수학 라이브러리인 Mathlib이 빠르게 성장하고 있고, 이걸 기반으로 AI 학습 데이터를 만드는 선순환이 일어나고 있어요.

한국 개발자에게 주는 시사점

AI와 형식 추론의 결합은 장기적으로 소프트웨어 개발 방식을 바꿀 수 있는 기초 기술이에요. 당장 실무에 적용할 건 아니지만, 이 흐름을 이해해두면 AI 코딩 도구가 어떤 방향으로 진화할지 감을 잡을 수 있어요. 관심이 있다면 Lean 4 튜토리얼을 한번 해보는 것도 좋고, AI가 수학 문제를 어떻게 접근하는지 DeepMind의 논문들을 훑어보는 것도 추천해요.