AI가 수학의 한복판에 들어왔어요 — '증명한다'는 게 뭔지 다시 묻는 중

무슨 이야기냐면요

수학은 오랫동안 '사람의 순수한 머리로 하는 일'의 상징이었어요. 그런데 요즘 AI가 수학의 한복판으로 들어오면서, 수학자들 사이에서 좀 묵직한 질문들이 터져 나오고 있어요. 단순히 'AI가 계산을 빨리 해준다' 수준이 아니에요. '증명이란 무엇인가', '이해한다는 게 뭔가', '앞으로 수학자의 역할은 뭔가' 같은, 학문의 뿌리를 건드리는 질문들이거든요.

AI가 수학에 들어오는 두 갈래

AI가 수학을 돕는 방식은 크게 두 갈래로 나눌 수 있어요. 하나는 증명 보조기(theorem prover)예요. 대표적으로 Lean이라는 도구가 있는데요. 이게 뭐냐면, 수학 증명을 컴퓨터가 한 줄 한 줄 검사할 수 있는 엄밀한 언어로 적게 해주는 거예요. 사람이 쓴 증명은 '이 정도면 맞겠지' 하고 넘어가는 빈틈이 생기기 쉬운데, Lean으로 옮겨서 끝까지 통과하면 '논리적으로 단 한 군데도 틈이 없다'는 게 기계로 보장돼요. 다른 한 갈래는 요즘 화제인 대규모 언어 모델(LLM)과 전용 AI예요. 구글 딥마인드가 만든 AlphaProof와 AlphaGeometry 같은 시스템은 국제수학올림피아드 수준의 어려운 문제를 거의 메달권으로 풀어내서 사람들을 놀라게 했어요. 즉, 한쪽은 '맞는지 검사'를, 다른 한쪽은 '아이디어 자체를 생성'하는 걸 도와주는 거예요.

그래서 어떤 큰 질문이 생기냐면요

여기서 골치 아픈 질문이 시작돼요. 만약 AI가 10만 줄짜리 증명을 내놨는데, 그게 기계 검사는 통과했지만 사람은 아무도 끝까지 못 읽는다면, 그걸 '증명됐다'고 말할 수 있을까요? 수학에서 증명은 단순히 '참임을 확인하는 것'을 넘어서 '왜 그런지 이해하게 해주는 것'이라는 전통이 있거든요. 기계가 참이라고 도장은 찍어줬는데 인간의 이해는 하나도 안 늘었다면, 그게 우리가 원하던 수학일까요? 사실 이건 완전히 새로운 고민은 아니에요. 1976년 '4색 정리'가 컴퓨터의 도움으로 처음 증명됐을 때도, 많은 수학자가 '사람이 검산할 수 없는 증명을 믿어도 되냐'며 논쟁했거든요. AI는 그 논쟁을 훨씬 큰 규모로 다시 불러온 셈이에요.

수학자의 역할은 어떻게 바뀔까요

현장 수학자들의 반응은 갈려요. 어떤 이들은 AI를 강력한 '조수'로 봐요. 지루한 경우 나누기나 막힌 보조정리를 AI한테 맡기고, 자기는 큰 그림과 통찰에 집중하는 거죠. 실제로 저명한 수학자들도 증명 보조기와 AI를 일상 연구에 끼워 넣기 시작했어요. 반대로 어떤 이들은 걱정해요. 아이디어를 떠올리는 일까지 AI가 점점 잘하게 되면, 수학자가 '문제를 푸는 사람'에서 'AI가 낸 답을 관리하고 검수하는 사람'으로 바뀌는 거 아니냐는 거죠. 어느 쪽이든, 수학을 '하는 방식' 자체가 바뀌고 있다는 데는 대부분 동의해요.

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

이 흐름이 순수 수학자만의 이야기는 아니에요. 첫째, Lean 같은 형식 검증(formal verification) 도구는 소프트웨어에도 그대로 쓰여요. 금융이나 항공, 보안처럼 버그가 치명적인 분야에서는 '코드가 명세대로 동작함'을 수학적으로 증명하는 게 점점 중요해지고 있거든요. Lean이나 Coq 같은 도구를 익혀두면 분명히 쓸모가 있어요. 둘째, 'AI가 낸 결과를 어디까지 믿을 것인가'라는 질문은 수학만의 고민이 아니라, AI가 짜준 코드를 리뷰하는 우리 모두의 고민과 똑같아요. 생성은 AI에게 맡기되 검증은 엄밀한 도구로 잡는다는 발상은, 코딩 에이전트 시대에 그대로 적용되는 교훈이에요.

마무리

정리하면, AI는 수학에서 '검증'과 '발상' 양쪽을 동시에 흔들면서, 증명과 이해의 의미를 다시 묻게 만들고 있어요. 이건 결국 '인간이 무엇을 잘해야 하는가'에 대한 질문이기도 해요. 여러분은 AI가 짜준 코드나 풀어준 문제를, 내용을 다 이해하지 못해도 '테스트만 통과하면' 믿고 쓰는 편인가요? 어디까지가 괜찮은 선일까요?