현대 사회의 금융, 통신, 물류 시스템은 모두 대규모 컴퓨터 네트워크 위에서 작동한다. 계산 능력은 이제 문명의 핵심 인프라가 됐다. 

바둑에서 인간이 밀렸을 때 사람들은 충격을 받았다. 계산과 직관의 게임에서 기계가 인간 최고수를 넘어섰기 때문이다. 그러나 바둑은 승패가 눈앞에 드러나는 게임이다. 

수학은 다르다. 수학은 답을 맞히는 학문이 아니라, 왜 그것이 참인지 증명하는 학문이다.

증명의 세계가 기계로

이제 인공지능은 계산을 넘어 증명의 영역으로 들어오고 있다. 

구글의 AI 연구조직인 구글 딥마인드(Google DeepMind)는 2024년 알파프루프(AlphaProof)와 알파지오메트리2(AlphaGeometry 2)가 국제수학올림피아드(IMO) 문제 6개 중 4개를 해결해 은메달 수준의 성과를 냈다고 발표했다. 

이후 네이처에 게재된 논문도 이 시스템이 42점 만점 중 28점을 얻어 은메달권 성과를 냈다고 설명했다.

2025년에는 한 걸음 더 나아갔다. 

구글 딥마인드는 제미나이 딥싱크(Gemini Deep Think)가 국제수학올림피아드에서 6문제 중 5문제를 해결해 35점을 얻었고, 금메달 수준에 도달했다고 밝혔다. 

로이터도 2025년 7월 구글과 오픈AI(OpenAI)의 AI 모델이 국제수학올림피아드에서 금메달 수준 성과를 냈다고 보도했다. 다만 오픈AI의 경우 공식 참가 방식이 아니라 별도 평가 결과라는 점은 구분할 필요가 있다.

중요한 것은 점수만이 아니다. 수학에서 AI가 성과를 냈다는 말은 단순히 어려운 문제의 답을 맞혔다는 뜻이 아니다. 인간 이성의 가장 엄격한 영역으로 여겨졌던 증명의 세계에 기계가 들어왔다는 뜻이다. 

수학은 오랫동안 인간 지성의 최후 보루처럼 여겨졌다. 정답보다 중요한 것은 논리였고, 논리보다 중요한 것은 검증이었다. 그런데 이제 그 검증의 과정에도 AI가 들어오기 시작했다.

기계에 대한 증명은 누가?

수학 증명은 일종의 신뢰 계약이다. 어떤 수학자가 새로운 정리를 발표하면 다른 수학자들이 그 증명을 읽고, 오류를 찾고, 논리의 빈틈을 검토한다. 

시간이 지나도 반례가 나오지 않고 공동체가 받아들이면 그 명제는 수학 지식의 일부가 된다. 수학의 권위는 개인의 명성에서 나오지 않는다. 검증 가능한 논리와 공동체의 승인에서 나온다.

AI가 이 구조를 흔드는 이유는 여기에 있다. 

AI가 만든 증명이 있다. 형식 검증 프로그램도 오류가 없다고 판단했다. 그런데 인간 수학자들이 그 증명의 전체 흐름을 직관적으로 이해하지 못한다면 어떻게 해야 하는가. 

기계가 맞다고 한 증명을 인간이 받아들이면, 그것은 인간이 이해한 지식인가. 아니면 기계가 보증한 지식인가.

여기서 ‘형식 검증’이라는 말이 중요하다. 

형식 검증은 수학 명제와 증명을 컴퓨터가 읽을 수 있는 엄격한 언어로 바꾸고, 논리 규칙에 따라 증명이 맞는지를 확인하는 방식이다. 리인(Lean·수학 증명 보조 프로그램) 같은 시스템이 대표적이다. 

리인 공식 소개도 리인을 “올바르고 유지 가능하며 형식적으로 검증된 코드”를 가능하게 하는 오픈소스 프로그래밍 언어이자 증명 보조 도구로 설명한다.

겉으로 보면 이는 수학자에게 좋은 일이다. 

인간이 놓칠 수 있는 논리적 빈틈을 기계가 잡아낼 수 있다. 방대한 경우의 수를 빠르게 검토할 수도 있다. 새로운 패턴이나 추측을 제안할 수도 있다. 오래 걸리던 검증 절차가 빨라지면 수학 연구의 속도도 올라갈 수 있다. 

그러나 속도가 곧 이해를 뜻하지는 않는다. 수학은 단순히 참과 거짓을 가르는 기계적 절차가 아니다. 왜 그런 구조가 성립하는지, 그 명제가 다른 이론과 어떤 관계를 갖는지, 어떤 방식으로 일반화될 수 있는지를 이해하는 과정이다. 

AI가 증명을 찾아냈다고 해서 인간의 이해가 자동으로 따라오는 것은 아니다.

이 지점에서 수학의 오래된 질문이 다시 살아난다. 

증명은 무엇인가. 논리적으로 오류가 없으면 충분한가. 아니면 인간이 납득할 수 있는 설명이어야 하는가. 컴퓨터가 검증한 긴 증명과 사람이 이해한 짧은 증명은 같은 권위를 갖는가. 기계가 만든 증명이 참이라면, 그 참의 의미는 누가 해석하는가.

인간에게 남은 질문

AI는 이 질문을 수학 바깥으로도 밀어낸다. 

오늘의 사회는 이미 이해보다 검증 절차에 의존하는 방향으로 가고 있다. 

금융 거래는 암호와 알고리즘 위에서 움직인다. 의료 진단과 신약 개발도 데이터와 모델의 판단을 참고한다. 선거 시스템도 전산 절차와 검증 장치에 의존한다. 

인간이 모든 과정을 직접 이해하지 못해도, 절차가 신뢰할 수 있다면 결과를 받아들이는 구조가 확대되고 있다.

수학은 그 흐름의 가장 엄격한 시험대다. 

수학에서조차 인간이 모든 증명을 직접 이해하지 못하고 기계 검증에 의존하게 된다면, 다른 지식 분야에서는 더 큰 변화가 일어날 수밖에 없다. 

과학 논문, 법률 판단, 금융 리스크 분석, 정책 시뮬레이션도 같은 질문 앞에 서게 된다. AI가 내놓은 결론을 인간은 어디까지 받아들일 수 있는가. 

그렇다고 AI를 수학의 침입자로만 볼 필요는 없다. 오히려 AI는 인간 수학자의 경쟁자라기보다 새로운 검증 도구에 가깝다. 

계산기가 암산을 대체했지만 수학을 없애지 않았듯, 증명 보조 AI도 수학자를 없애기보다 수학자의 역할을 바꿀 가능성이 크다. 

인간은 더 이상 모든 계산과 검토를 손으로 반복하지 않아도 된다. 대신 어떤 문제를 물을지, 어떤 증명이 의미 있는지, 어떤 결과를 지식으로 채택할지 결정해야 한다.

이 변화는 교육에도 영향을 준다. 

앞으로 수학 교육은 정답을 빨리 구하는 훈련만으로는 부족해질 수 있다. AI가 풀이를 제시하는 시대에는 “답을 냈는가”보다 “왜 그 답을 믿을 수 있는가”가 더 중요해진다. 

학생은 계산자가 아니라 검증자가 되어야 한다. 풀이를 외우는 능력보다 논리의 빈틈을 찾는 능력이 더 중요해질 수 있다.

ALO(AI Linked Optimization) 관점에서 보면 이 변화의 핵심은 분명하다. 

AI는 증명의 생산과 검토를 도울 수 있다. 그러나 어떤 증명을 지식으로 채택할지, 어떤 설명을 교육할지, 어떤 오류 가능성을 감수할지는 인간의 결정 영역이다. 

수학도 AI시대에 들어섰지만, 참을 받아들이는 마지막 책임까지 기계에 넘길 수는 없다.

AI가 수학을 흔드는 것은 계산 능력 때문이 아니다. 인간이 무엇을 참이라고 인정하는가라는 검증의 구조를 다시 묻게 만들기 때문이다. 

수학은 정답의 학문처럼 보이지만, 사실은 신뢰의 학문이다. 그리고 신뢰는 기계가 대신 만들어줄 수 없다. 기계는 검증을 도울 수 있지만, 검증을 신뢰로 바꾸는 최종 결정은 인간 공동체의 몫이다.

AI시대의 수학은 인간 이성의 패배가 아니다. 오히려 인간 이성이 어디에 남아야 하는지를 더 선명하게 보여준다. 계산은 기계가 할 수 있다. 증명도 기계가 도울 수 있다. 

그러나 질문을 세우고, 의미를 해석하고, 참을 받아들이는 책임은 인간에게 남는다.

수학도 AI시대에 들어섰다. 이제 중요한 질문은 AI가 증명을 할 수 있느냐가 아니다. 그 증명을 누가 검증하고, 누가 받아들이며, 누가 책임질 것인가다.

❄ 이 기사는 주잔 한미일보 제 9호(5월 2주차)에 실린 기사입니다.