---
title: AI가 수학 난제를 풀었다는데, 정확히 무엇을 풀었을까 — 헤드라인을 갈래별로 나눠 보고, 수식을 넣으면 풀고 검산까지 하는 엔진을 만들었다
url: https://oosioo.com/p/ai%EA%B0%80-%EC%88%98%ED%95%99-%EB%82%9C%EC%A0%9C%EB%A5%BC-%ED%92%80%EC%97%88%EB%8B%A4%EB%8A%94%EB%8D%B0-%EC%A0%95%ED%99%95%ED%9E%88-%EB%AC%B4%EC%97%87%EC%9D%84-%ED%92%80%EC%97%88%EC%9D%84%EA%B9%8C
date: 2026-10-16T13:04:12+00:00
author: SYSOP
summary: 「90년 난제를 88시간 만에」, 「리만 가설 증명 포함」 같은 제목이 한 달에도 몇 번씩 나온다. 그런데 같은 「풀었다」 안에는 답이 정해진 시험 문제, 점수로 채점되는 탐색, 이미 있던 논문 찾기, 진짜 미해결 문제가 뒤섞여 있다. 수학 문제를 푼다는 게 어떤 일인지부터 짚고, 2026년에 실제로 무엇이 풀렸고 무엇이 부풀려졌는지 갈라 봤다. 수능·SAT 문제를 푸는 AI가 어떻게 도는지도 정리했고, TeX로 식을 넣으면 풀이 단계와 검산을 보여 주는 작은 엔진을 직접 만들어 붙였다.
---
# AI가 수학 난제를 풀었다는데, 정확히 무엇을 풀었을까 — 헤드라인을 갈래별로 나눠 보고, 수식을 넣으면 풀고 검산까지 하는 엔진을 만들었다

![이 글의 풀이 엔진 화면. f(x)=x³−3x²+2 를 읽고 f′(x)=3x²−6x 로 미분한 뒤, 「한쪽으로 모으기」「인수분해」 단계를 거쳐 3x(x−2)=0 을 보여 준다](/uploads/31232cade748a941.webp)

지난달 신문 제목들을 모아 보면 수학은 이미 끝난 학문 같다. 「90년 수학 난제, AI가 88시간 만에 풀었다」, 「오픈AI, 300여 개 수학 난제 돌파… 리만 가설 증명 포함」, 「50년 수학 난제 15분 만에 푼 AI」. 그런데 같은 달 필즈상 수상자 스물다섯 명이 AI 회사들의 수학 경쟁이 수학을 해치고 있다는 성명을 냈다. 둘 중 하나가 틀린 걸까.

둘 다 사실이다. 다만 「풀었다」라는 말 하나가 너무 많은 일을 덮고 있다. 시험 문제를 맞힌 것, 점수가 매겨지는 탐색에서 더 좋은 답을 찾은 것, 이미 누가 풀어 둔 논문을 찾아낸 것, 아무도 몰랐던 정리를 증명한 것이 기사 제목에서는 전부 「난제를 풀었다」가 된다.

## 무엇을 하려 했나

세 가지를 하고 싶었다. 첫째, 수학 문제를 실제로 푼다는 게 어떤 작업들로 이뤄지는지 정리하고 그중 어디를 AI가 잘 돕는지 가른다. 둘째, 2023년부터 지금까지 「AI가 수학을 풀었다」는 발표를 갈래별로 나눠, 무엇이 진짜 진보고 무엇이 부풀려졌는지 본다. 셋째, 수능이나 SAT 수학을 푸는 AI는 어떻게 돌아가는지 알아보고, 그 원리를 보여 줄 작은 엔진을 직접 만든다. 엔진은 TeX로 식을 넣으면 읽고, 어떤 문제인지 가르고, 교과서 순서로 풀고, 답을 원래 식에 다시 넣어 검산한다.

## 수학 문제를 푼다는 건 어떤 일인가

시험 문제와 연구 문제는 같은 「문제」라는 이름을 쓰지만 하는 일이 다르다. 시험 문제는 답이 있고, 출제자가 그 답에 이르는 길을 이미 안다. 연구 문제는 답이 있는지도 모른다. 수학자가 하는 일을 순서대로 늘어놓으면 대략 이렇다.

1. 문제 고르기 — 풀 만하고 풀 가치가 있는 질문을 찾는다
2. 작은 경우 계산하기 — n=1, 2, 3을 손으로 혹은 컴퓨터로 돌려 본다
3. 규칙 찾기와 추측 — 숫자 사이에서 패턴을 읽고 「아마 늘 이럴 것이다」라고 적는다
4. 반례 찾기 — 그 추측을 깨는 경우가 있는지 뒤진다
5. 증명 전략 세우기 — 비슷한 문제에서 통한 방법을 빌려 오거나 새 도구를 만든다
6. 보조정리로 쪼개기 — 큰 증명을 작은 단계들로 나눈다
7. 검증 — 단계마다 빈틈이 없는지 확인한다
8. 심사 — 다른 전문가가 몇 달씩 읽는다
9. 글쓰기 — 남이 이해하고 이어서 쓸 수 있게 정리한다

조지 폴리아가 1945년 『어떻게 문제를 풀 것인가』에서 이해·계획·실행·되돌아보기라는 네 단계로 요약한 것을 연구 쪽으로 늘린 모양이다. 윌리엄 서스턴은 1994년 글에서 수학의 목적이 증명 그 자체가 아니라 사람의 이해를 넓히고 그 이해를 남에게 전하는 데 있다고 썼다. 9번이 빠지면 수학자들은 일이 끝났다고 보지 않는다.

이 목록에서 사람들이 잘 안 보는 쪽이 7번과 8번이다. 검증이 일의 큰 몫을 차지한다.

- **페르마의 마지막 정리**: 앤드루 와일스가 1993년 6월 증명을 발표했다. 심사 중에 빈틈이 발견됐고, 그걸 메우는 생각이 나온 게 1994년 9월이다. 논문은 1995년에 실렸다
- **케플러 추측**(공을 가장 빽빽하게 쌓는 법): 토머스 헤일스가 1998년 증명을 냈다. 심사위원 열두 명 남짓이 4년 가까이 들여다보고 「99% 확신한다」는 말을 남긴 채 완전한 확인을 포기했다. 헤일스는 컴퓨터로 증명을 한 줄씩 검사하는 프로젝트를 따로 꾸렸고, 그게 끝난 게 2014년이다
- **불리언 피타고라스 세 수 문제**: 2016년 SAT 풀이기(참·거짓 조합을 기계적으로 뒤지는 프로그램)가 7,825에서 답이 바뀐다는 걸 보였다. 코어 800개로 이틀을 돌렸고, 증명 파일이 200 TB에 가깝다. 답이 맞는다는 건 기계가 확인했지만 왜 하필 7,825인지는 아무도 모른다

AI가 수학을 「돕는다」는 말은 이 아홉 단계 가운데 어디를 돕느냐로 갈라 봐야 한다. 2번과 4번(계산과 반례 찾기)은 컴퓨터가 수십 년째 해 온 일이다. 7번은 검사기(Lean 같은 형식 증명 언어)가 생기면서 기계 몫이 됐다. 1번과 9번은 여전히 사람 몫이다. 2026년의 새 소식은 5번과 6번, 그러니까 증명의 뼈대를 AI가 세우기 시작했다는 데 있다.

## 같은 「풀었다」, 서로 다른 다섯 가지 일

![가로축은 결과가 맞는지 확인하는 데 드는 품(기계가 즉시 판정 ~ 전문가 여럿이 몇 달), 세로축은 문제가 얼마나 열려 있었나(답이 이미 있다 ~ 아무도 모른다). 수능·IMO·에르되시 소동은 아래, FunSearch·AlphaEvolve와 Lean 형식화는 왼쪽, 2026년의 단위거리 반증·나비에-스토크스·719편 원고는 오른쪽 위에 있다](/uploads/83f27d045d9eb1f0.webp =760)

지난 3년 동안 나온 발표를 문제 종류로 나누면 다섯 갈래가 나온다.

### 1. 답이 정해진 시험 문제

국제수학올림피아드(IMO)가 대표다. 2024년 구글 딥마인드의 AlphaProof는 42점 만점에 28점으로 은메달 선을 넘었다. 다만 사람이 문제를 형식 증명 언어인 Lean으로 옮겨 줬고, 학생들이 4시간 반씩 두 번 푸는 동안 AI는 문제에 따라 사흘까지 썼다. 2025년에는 구글의 Gemini Deep Think가 사람과 같은 시간 안에, 사람이 쓰는 문장으로 35점을 받아 IMO 공식 채점으로 금메달 기준을 넘었다. OpenAI도 같은 점수를 발표했지만 공식 채점을 받지 않았고, 폐막식 전에 발표해 논란이 됐다.

어려운 문제인 건 맞다. 하지만 출제자가 답과 풀이를 이미 아는 문제다.

### 2. 점수로 채점되는 탐색

딥마인드의 FunSearch(2023)와 AlphaEvolve(2025)가 여기 속한다. AI가 프로그램을 써서 후보를 만들면, 미리 짜 둔 채점 함수가 점수를 매기고, 점수 좋은 후보를 바탕으로 다시 만든다. AlphaEvolve는 4×4 복소수 행렬 곱셈을 곱셈 48번으로 하는 방법을 찾아, 1969년 슈트라센 방식(49번)을 처음으로 이겼다. 50개 넘는 열린 문제에 넣었더니 약 75%는 이미 알려진 최고 기록을 다시 찾았고 약 20%는 기록을 고쳤다.

이건 「더 좋은 예를 찾는」 일이다. 찾은 예가 기록을 넘는지는 계산 한 번으로 확인된다. 그래서 AI가 가장 강하다. 2025년 테렌스 타오 등이 같은 도구를 67개 문제에 돌린 논문을 냈는데, 결과가 좋으냐 나쁘냐는 전문가가 지시문에 어떤 귀띔을 넣느냐에 크게 달렸다고 적었다.

### 3. 이미 있던 답을 찾은 것

2025년 10월 OpenAI 부사장이 「GPT-5가 에르되시 미해결 문제 10개를 풀었다」고 올렸다가 지웠다. 문제 목록을 관리하는 수학자 토머스 블룸은 「극적인 오도」라고 했다. 목록에 「미해결」이라고 적힌 건 블룸 본인이 해법 논문을 모른다는 뜻이었고, GPT-5는 이미 문제를 푼 옛 논문을 찾아냈을 뿐이었다. 딥마인드의 데미스 허사비스는 한 마디로 「민망하다」고 했다.

문헌 찾기는 실제로 쓸모가 있다. 수학자들도 반긴다. 다만 새 수학은 아니다.

### 4. 아는 정리를 기계가 검사할 수 있게 옮긴 것

Lean은 증명을 한 줄씩 기계가 검사하게 해 주는 언어다. 사람이 쓴 증명을 Lean으로 옮기는 일(형식화)은 고되기로 유명하다. 2025년 Math Inc라는 회사는 자사 에이전트가 타오 등이 18개월째 붙들고 있던 「강한 소수 정리」 형식화를 3주 만에 끝냈다고 발표했다. 이미 증명된 정리를 옮긴 것이라 새 결과는 아니지만, 이 일이 빨라지면 다음 갈래의 검증이 싸진다.

### 5. 진짜 아무도 몰랐던 문제

여기서부터가 2026년에 달라진 부분이다. 2025년까지는 「AI가 난제를 풀었다」는 기사 대부분이 위 넷 중 하나였다. 2026년에는 다섯째 갈래가 실제로 나왔다.

- **단위거리 추측 반증**(5월): 에르되시가 1946년에 낸 추측을 OpenAI 모델이 깼다. 노가 알론, 팀 가워스, 멜라니 우드 등 외부 수학자들이 검증하고 짧게 다시 쓴 논문을 따로 냈다
- **사이클 이중 덮개 추측**(7월): 50년 묵은 그래프 이론 추측의 증명을 OpenAI 모델이 냈고, 짐 길런과 IBS의 엄상일 교수 등 그래프 이론 연구자들이 증명을 읽고 더 쉽게 풀어 쓴 해설 논문을 냈다

가워스는 단위거리 반증을 두고 AI 수학의 이정표라고 했다. 이 둘은 과장이 아니다.

## 2026년 가을, 헤드라인과 명제 사이

문제는 그다음이다. 진짜 결과가 몇 개 나오자 그 뒤의 발표들이 같은 무게로 보도되기 시작했다.

**나비에-스토크스(9월)**. 유체의 움직임을 나타내는 방정식에서 해가 유한한 시간 안에 터질 수 있느냐는, 클레이 연구소가 상금 100만 달러를 건 일곱 문제 중 하나다. OpenAI는 해가 터지는 예를 만들었다고 발표했고, 약 1만 개 에이전트가 88시간을 돌렸다고 알려졌다. 사이언티픽 아메리칸에 따르면 이 증명은 유체 바깥에서 힘(외력)을 가하는 판본에 대한 것이다. 2000년 문제문은 외력을 허용하는 선택지를 두고 있어서 공식 문구로는 해당하지만, 대부분의 전문가가 붙들어 온 건 외력이 없는 판본이다. 시카고대의 루이스 실베스트레는 「클레이 문제는 해결됐지만, 나비에-스토크스의 핵심 문제는 해결되지 않았다」고 했다. 외력을 만들어 해를 터뜨리는 기법 자체도 디에고 코르도바와 루이스 마르티네스-소로아가 먼저 만들었다.

**719편 원고(10월)**. OpenAI가 내부 모델로 만든 수학 원고를 GitHub에 한꺼번에 올렸다. 저장소 설명에 따르면 약 4,000개 문제를 던져 결과 묶음 372개, 원고 719편이 나왔고, 결과 하나에 평균 세 시간쯤 걸렸다. 대표 결과 가운데 Lean으로 기계 검사를 마친 건 약 42%이고, 설명서에는 「형식화되지 않은 결과 일부는 문제가 있을 수 있다」고 적혀 있다.

![던진 문제 약 4,000개, 결과 묶음 372개(원고 719편), 그중 Lean으로 형식화된 대표 결과 약 42%를 막대로 비교한 그림](/uploads/35b049b2cf7a3482.webp =720)

그 안에 「준리만 가설」이라는 결과가 있다. 리만 가설은 제타 함수의 (자명하지 않은) 영점이 전부 실수부 1/2 직선 위에 있다는 주장이다. 이번 결과는 실수부가 7/8보다 큰 곳에는 영점이 없다는 것이다. 사실로 확인되면 지금까지 아무도 못 넘은 벽을 넘은 것이라 일부 수학자는 「사람이 했으면 즉시 필즈상」이라고 했지만, 리만 가설과는 다른 명제다. 이 결과를 이어받아 경계를 0.87496쯤으로 조금 더 당긴 사람의 논문도 벌써 나왔다. 그런데 국내 기사에는 「리만 가설 증명 포함」으로 실렸다.

**필즈상 수상자 성명(9월)**. 타오의 블로그에 실린 「AI와 수학의 심각한 어긋남」에는 허준이, 페터 숄체, 마리나 뱌조우스카 등 스물다섯 명이 이름을 올렸다. AI가 어려운 문제를 풀 수 있다는 건 부정하지 않는다. 문제 하나 푸는 건 수단이고 목적은 이해인데, 유명 난제를 홍보 수단으로 쓰면서 앞선 연구를 밝히지 않고 남이 읽을 수 있는 글도 없이 서둘러 발표하는 걸 문제 삼았다. 국내에서는 「인간 역할 위협 경고」로 보도됐다.

정리하면 2026년 기사를 읽을 때 물어야 할 건 세 가지다.

- **무엇을 증명했나.** 원래 문제인가, 좁힌 판본인가 (외력판, 7/8, 일부 경우로 한정한 호지 추측)
- **누가 어떻게 확인했나.** 외부 전문가가 읽었나, Lean이 검사했나, 아니면 발표한 회사만 확인했나
- **몇 개 중에 몇 개인가.** 4,000개를 던져 고른 결과인가. 실패는 발표되지 않는다

타오는 올해 초 「지금 AI로 최소한의 도움만으로 풀릴 만큼 쉬운 에르되시 문제는 열린 문제의 1~2% 정도」라고 했다. 50년 동안 안 풀렸다는 게 50년 동안 아무도 안 들여다봤다는 뜻일 수도 있다는 말도 붙였다.

## AI가 잘하는 자리는 검증이 싼 자리다

다섯 갈래를 나란히 놓으면 공통점이 보인다. **결과가 맞는지 기계가 싸게 확인할 수 있는 곳**에서 AI가 가장 먼저, 가장 크게 이겼다. 정답 번호가 있는 시험, 점수 함수가 있는 탐색, Lean 검사기가 판정하는 형식 증명이 그렇다. 확인이 싸면 수천 번 틀려도 괜찮다. 수천 번 시도해서 맞은 것만 남기면 되기 때문이다.

반대로 확인이 비싼 곳에서는 AI가 틀린 증명을 그럴듯하게 많이 내놓는 것 자체가 부담이 된다. 2025년 3월 ETH 취리히 연구진이 미국 수학올림피아드(USAMO) 문제의 증명을 사람이 채점했더니, 정답 맞히기 시험에서 높은 점수를 받던 모델들이 증명 채점에서는 Gemini 2.5 Pro만 25%, 나머지는 5% 아래였다. 틀린 단계를 자신 있게 「증명 끝」이라고 적는 일이 흔했다. 그 뒤로 모델은 빠르게 나아졌지만, 확인이 비싸다는 사정은 그대로다. 719편을 누가 다 읽을 것인가가 지금 수학계의 고민이다.

Lean이 이 문제를 풀어 줄 것 같지만 절반만 푼다. Lean은 「이 증명이 이 명제를 따른다」는 건 보장하지만, 「이 명제가 우리가 묻던 그 질문인가」는 보장하지 않는다. 나비에-스토크스 논쟁이 정확히 그 틈에서 벌어졌다.

| 문제 | 무엇을 묻나 | AI와 관련된 진전 (2026년 10월 기준) |
|---|---|---|
| 리만 가설 | 제타 함수 영점이 모두 1/2 선 위에 있나 | 사람이 수치로 3조 높이까지 확인. 증명 진전 없음. 7/8 경계 결과는 별개 명제이고 검증 중 |
| P 대 NP | 빨리 검사되는 문제는 빨리 풀리기도 하나 | 없음 |
| 나비에-스토크스 | 외력 없는 유체 방정식의 해가 터지나 | 외력판은 AI가 터지는 예를 냈다고 발표(논쟁 중). 외력 없는 판은 미해결 |
| 쌍둥이 소수 | 차이가 2인 소수 쌍이 끝없이 있나 | 간격 246까지는 사람이 증명(2014). AI 기여 없음 |
| 콜라츠 추측 | 3n+1 규칙이 늘 1로 끝나나 | 2⁷¹까지 컴퓨터로 확인(2025). 유한한 확인은 증명이 아니다 |
| 에르되시 문제들 | 조합·정수론의 수많은 작은 질문 | AI가 실제로 여러 개 풂. 대부분 쉬운 쪽 꼬리(타오) |

## 수능·SAT 문제를 푸는 AI는 어떻게 도나

시험 문제를 푸는 기계에는 계보가 둘 있다.

**첫째, 계산기 계보.** 매스매티카, 울프럼 알파, 파이썬의 SymPy 같은 컴퓨터 대수 시스템(CAS)이다. 식을 나무 모양 자료로 들고 1/3이나 √2를 소수로 바꾸지 않은 채 다룬다. 그래야 「이 식이 정확히 0인가」를 판정할 수 있다. 인수분해, 미분, 적분, 극한을 수백 년 쌓인 규칙과 알고리즘으로 처리한다. 사진을 찍으면 풀어 주는 앱들은 대개 사진 속 식을 글자(대개 LaTeX)로 읽어 내는 수식 인식을 앞에 붙인다. 국내 앱 콴다의 기술 책임자는 2021년 인터뷰에서 수식 인식과 함께 「문제은행식으로 이미지를 많이 쌓아 놓고 유사한 문제를 빨리 찾는 검색」이 핵심이라고 했다. 풀기보다 이미 풀린 비슷한 문제를 찾아 주는 쪽이다.

이 계보의 한계는 분명하다. 식이 주어져야 한다. 「곡선 위의 점 P에서 그은 접선이 y축과 만나는 점을 Q라 할 때…」 같은 문장을 식으로 바꾸는 일, 즉 모델링은 못 한다. 수능 4점짜리 문항은 대부분 여기서 갈린다.

**둘째, 언어모델 계보.** 이쪽은 문장을 읽는 데서 출발한다. 2022년 이후 점수를 끌어올린 방법을 차례로 적으면 이렇다.

- **풀이 과정 쓰게 하기**(2022): 답만 말하게 하지 않고 단계를 쓰게 하면 큰 모델의 정답률이 크게 오른다
- **여러 번 풀고 다수결**(2022): 같은 문제를 수십 번 풀게 해 가장 많이 나온 답을 고른다
- **계산은 도구에 맡기기**(2022~2023): 언어모델은 곱셈 자리올림 같은 데서 잘 틀린다. 그래서 식을 세우는 데까지만 하고 계산은 파이썬이나 SymPy를 불러서 시킨다. 첫째 계보를 둘째 계보가 부하로 쓰는 셈이다
- **단계마다 채점하기**(2023): 답이 아니라 풀이 각 줄이 맞는지 판정하는 채점 모델을 따로 훈련한다
- **정답만으로 강화학습**(2024~2025): 답이 맞으면 상, 틀리면 벌만 주고 스스로 풀이를 길게 쓰게 훈련한다. 답을 기계가 채점할 수 있는 수학이 이 방법에 딱 맞는다

![DeepSeek-R1 논문의 미국 수학경시 AIME 2024 정답률. 강화학습 전 15.6%, 정답 채점만으로 강화학습한 R1-Zero 71.0%, 최종 R1 79.8%](/uploads/2ac31311950d006d.webp =720)

마지막 방법이 지금 시험 수학 성적이 크게 오른 직접적인 이유다. 여기서도 「검증이 싸다」가 열쇠다. 답이 0~999 사이 정수인 경시대회나 5지선다·단답형인 수능은 기계가 채점할 수 있어서, 모델은 수백만 번 풀고 맞은 길만 강화한다.

수능에서는 어떨까. 연합뉴스가 연세대 김시호 교수팀과 함께 2026학년도 수능을 무료판 챗봇들에게 풀렸다. 인터넷 검색을 막고, 수식은 LaTeX로 넣고, 표와 그림은 PDF로 줬다. ChatGPT(GPT-5)가 수학 확률과 통계 96점, 미적분 92점, 기하 84점을 받았다. 2023학년도에 GPT-3.5가 받은 17점과 비교하면 3년 사이 일이다. 그런데 EBS와 입시업체가 고난도로 꼽은 여섯 문항은 ChatGPT가 확률과 통계 30번 하나를 맞힌 것 말고는 모든 모델이 틀렸다. 딥시크는 표가 든 쉬운 문제도 틀렸는데, 문제를 잘못 읽은 것으로 보인다.

![2023학년도 GPT-3.5 수능 수학 17점과 2026학년도 GPT-5 무료판 확률과 통계 96점, 미적분 92점, 기하 84점을 비교한 막대그래프](/uploads/6b05995dd5216c22.webp =720)

네이버와 KAIST 연구진은 2014~2025년 수능 수학 664문항으로 시험지를 만들고, 그중 339문항에는 평가원이 공개한 문항별 실제 오답률을 붙였다(KCSAT-ML, 2026). 사람이 많이 틀린 문항일수록, 생각할 시간을 적게 준 모델의 정답률이 크게 무너졌다. 생각할 시간을 늘리면 쉬운 문항에서는 오히려 과하게 생각하다 틀리기도 했다. 미국 애플 연구진은 초등 문장제의 숫자만 바꾸거나 상관없는 문장 하나를 끼워 넣어도 모델 점수가 떨어진다고 보고했다(GSM-Symbolic, 2024). 수능에서 「AI가 만점」과 「AI가 킬러문항을 못 푼다」가 동시에 기사로 나오는 건, 어떤 모델에 어떤 설정을 줬느냐가 결과를 크게 바꾸기 때문이다.

## 직접 만든 엔진: 식을 넣으면 풀고, 다시 넣어 본다

첫째 계보, 식이 주어졌을 때 푸는 쪽을 직접 만들었다. 아래 칸에 TeX로 식을 넣고 「풀기」를 누르면 된다. 처음 누를 때 계산 엔진(브라우저 안에서 도는 파이썬과 SymPy)을 내려받느라 10~30초쯤 걸린다. 그 전에 예제 단추를 누르면 미리 풀어 둔 결과를 바로 볼 수 있다.

```map /embed/tex-solver-2026.html 3:4
이차방정식부터 극값 찾기, 정적분, Σ 합까지 예제 열두 개. 식을 고쳐 넣으면 읽기·분류·풀이·검산 네 단계를 다시 보여 준다. 입력은 이 화면 밖으로 나가지 않는다
```

엔진은 네 단계로 돈다.

1. **읽기.** `\frac{x^2-4}{x-2}` 같은 TeX 글자를 토막 내어 식 나무로 만든다. 곱셈 기호를 생략한 `2x`, `3(x+1)`, `\sin 2x` 같은 교과서 표기를 곱으로 읽는 규칙을 직접 짰다. 「식 나무 보기」를 펼치면 컴퓨터가 나눗셈을 「−1 제곱을 곱하기」로, 뺄셈을 「−1을 곱해 더하기」로 들고 있는 게 보인다
2. **분류.** 등호가 있으면 방정식, 줄이 둘 이상이면 연립방정식, 부등호면 부등식, `\lim`이면 극한, `\int`면 적분, `\sum`이면 급수로 가른다. `f(x)=…`로 시작하는 줄은 함수 정의로 받아 두고 다음 줄에서 `f'(x)`와 `f(2)`를 쓸 수 있게 했다
3. **풀이.** 교과서 순서대로 단계를 적는다. 이차방정식은 인수분해가 되면 인수분해로, 안 되면 판별식과 근의 공식으로 간다. 극한은 먼저 그냥 넣어 보고, 0/0이 나오면 약분이나 로피탈로, ∞−∞면 켤레식으로 간다. 실제 계산(인수분해, 적분, 극한값)은 SymPy가 하고, 어떤 단계를 어떤 말로 보여 줄지는 내가 정한 규칙이다
4. **검산.** 답을 원래 식에 다시 넣는다. 방정식은 해를 대입해 좌변−우변이 0인지 보고, 적분은 구간을 잘게 쪼개 직접 더한 수치와 비교하고, 부정적분은 결과를 다시 미분하고, Σ는 n=1, 2, 3, 7일 때 하나씩 더한 값과 공식을 맞춰 본다

이 네 단계는 앞에서 본 이야기의 축소판이다. 3단계(풀기)보다 4단계(확인하기)가 훨씬 싸다. 그리고 엔진이 「맞다」고 말할 수 있는 건 4단계 덕분이다.

## 어디서 틀렸나

- **삼각방정식의 해를 두 개만 냈다.** `2\sin x = 1`을 넣자 처음 판은 x=π/6, 5π/6 두 개를 내놓고 검산까지 「맞다」로 끝냈다. 둘 다 대입하면 맞으니 검산은 통과한다. 하지만 사인은 주기함수라 해가 끝없이 많다. 계산 도구의 기본 풀이 함수가 대표값만 돌려준 탓이다. 실수 전체에서 해의 모임을 구하게 바꾸고, 수능처럼 「0 ≤ x < 2π 안의 해」를 따로 적게 했다. **검산이 「맞다」고 해도 답이 다 나왔다는 뜻은 아니다.** 대입 검산은 내놓은 답이 틀렸는지만 잡고, 빠뜨린 답은 못 잡는다
- **지수방정식에서 허수 해를 같이 냈다.** `e^{2x}=e^{x}+2`에 x=ln 2와 함께 x=iπ가 나왔다. eˣ=−1을 복소수 범위에서 풀면 맞는 답이고, 대입 검산도 통과한다. 하지만 고등학교 지수방정식은 실수 범위에서 푼다. 다항방정식이 아닌 경우엔 허수 해를 걸러 내고 걸렀다고 적게 했다. 기계가 틀린 게 아니라 질문의 전제를 몰랐던 것이다
- **답은 맞고 설명이 틀렸다.** 극값 예제에서 `3x(x−2) = 0`을 보여 주며 「유리수 범위에서 더 쪼개지지 않는다」고 적었다. 이미 인수분해된 식을 받아서 「인수분해 전과 후가 같다」고 판단한 탓이다. 해는 x=0, 2로 맞았고 검산도 통과했다. 답 대조나 대입 검산으로는 이런 오류가 안 잡힌다. 앞에서 본 「정답은 맞히는데 증명은 틀리는」 언어모델과 같은 꼴의 실수다. 식을 펼친 뒤에 판단하게 고쳤다
- **절댓값에서 멈췄다.** `|x-3|=2`를 넣자 「풀지 못한다」며 멈췄다. 기호 x가 복소수일 수도 있다고 보면 |x−3|을 경우로 나눌 수 없다. 절댓값이 있으면 미지수를 실수로 두게 했다
- **5차 방정식에서 읽을 수 없는 답을 냈다.** `x^5-x+1=0`에 「CRootOf(x⁵−x+1, 0)」 같은 기호를 다섯 개 내놓았다. 틀린 답은 아니다. 「이 방정식의 0번째 근」이라는 뜻이다. 5차 이상은 일반적인 근의 공식이 없다(아벨–루피니 정리). 이럴 땐 그렇다고 적고 수치로 보여 주게 했다
- **처음 판은 방정식을 하나도 못 풀었다.** 등호를 TeX로 옮기는 표에 `=` 자체를 빠뜨려서, 부등식과 극한은 다 되는데 방정식 다섯 개가 전부 오류로 끝났다. 예제 스물여섯 개를 한꺼번에 돌리는 시험을 먼저 만들어 둔 덕에 바로 보였다

## 왜 한 줄로 되는가

식이 이미 주어진 문제는 수백 년 동안 다듬어진 규칙이 있고, 그 규칙은 오래전에 프로그램이 됐다. SymPy가 무료로 공개돼 있고, 그걸 브라우저 안에서 돌리는 도구(Pyodide)도 있다. 남은 일은 교과서 표기를 기계가 읽는 꼴로 바꾸는 것, 풀이를 사람이 보는 순서로 적는 것, 그리고 검산을 붙이는 것이다. 이 셋은 범위가 좁고 맞았는지 바로 확인되는 일이라 AI에 시키기 좋다. 이 엔진을 만드는 일 자체가 「검증이 싼 일」이었다.

## 따라 하려면

- **식을 먼저 세워라.** 문장제를 언어모델에 통째로 맡기기보다, 식을 세우는 데까지 쓰고 계산은 이런 엔진이나 울프럼 알파에 넘기면 덜 틀린다. 위에서 본 「계산은 도구에 맡기기」를 손으로 하는 셈이다
- **답을 원래 식에 넣어 보라.** 어느 AI든 답을 받으면 대입해 보는 버릇만으로 틀린 답 대부분을 걸러 낸다. 다만 빠뜨린 답은 대입으로 안 잡힌다. 삼각방정식, 근호가 든 방정식, 분수방정식은 범위와 조건을 따로 확인하라
- **기사를 읽을 땐 세 가지를 물어라.** 원래 문제인가 좁힌 판본인가, 누가 확인했나, 몇 개 중 몇 개인가

## 못 하는 것

- **문장과 그림을 못 읽는다.** 이 엔진은 식이 있어야 시작한다. 수능 4점짜리의 대부분은 식을 세우는 게 문제다
- **조건이 붙은 문제를 못 푼다.** 「실근이 세 개가 되도록 하는 k의 범위」 같은, 매개변수를 두고 경우를 나누는 문제는 아직 분류에 없다
- **증명을 못 한다.** 계산하고 확인할 뿐이다. 「모든 n에 대해」를 보이는 일은 이 엔진의 몫이 아니다
- **표기가 좁다.** 점의 좌표 (a, b), 행렬, 벡터, 이어 쓴 부등식 a < x < b는 아직 못 읽는다. 삼각방정식의 범위는 0 이상 2π 미만으로 고정이다
- **AI 수학의 현재를 판정하지 못한다.** 2026년 9~10월 발표들은 아직 검증 중이다. 이 글을 쓴 뒤에 철회되거나 확인되는 결과가 있을 수 있다

수학자들이 무서워하는 건 AI가 문제를 푸는 것보다 아무도 읽지 않은 증명이 쌓이는 쪽이다. 풀이는 딸깍으로 나와도 확인은 아직 딸깍이 안 된다. 그래서 이 작은 엔진에도 풀이보다 검산을 먼저 붙였다.

### 재미있게 읽었다면 꼭 의견을 달아달라.

## 출처

- 수학 연구의 단계: 폴리아 『How to Solve It』(1945, [Princeton University Press](https://press.princeton.edu/books/paperback/9780691164076/how-to-solve-it)) · Thurston, "On proof and progress in mathematics"(1994, [arXiv math/9404236](https://arxiv.org/abs/math/9404236))
- 검증 사례: 케플러 추측과 Flyspeck([Forum of Mathematics, Pi, 2017](https://www.cambridge.org/core/product/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC), [위키백과](https://en.wikipedia.org/wiki/Kepler_conjecture)) · 불리언 피타고라스 세 수([arXiv 1605.00723](https://arxiv.org/abs/1605.00723)) · 콜라츠 2⁷¹ 확인(Barina 2025, [브르노 공대](https://www.fit.vut.cz/research/publication/c197809/))
- IMO: [딥마인드 AlphaProof(2024)](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/) · [Gemini Deep Think 금메달(2025)](https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/)
- 탐색: [FunSearch(Nature, 2023)](https://www.nature.com/articles/s41586-023-06924-6) · [AlphaEvolve(2025)](https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/) · Georgiev·Gómez-Serrano·Tao·Wagner([arXiv 2511.02864](https://arxiv.org/abs/2511.02864))
- 에르되시 소동: [TechCrunch(2025-10-19)](https://techcrunch.com/2025/10/19/openais-embarrassing-math/) · 타오의 「1~2%」 발언([The Decoder](https://the-decoder.com/terence-tao-says-gpt-5-2-pro-cracked-an-erdos-problem-but-warns-the-win-says-more-about-speed-than-difficulty/)) · [AI 기여 집계 위키](https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems)
- 2026년 결과: 단위거리 반증 검증 논문([arXiv 2605.20695](https://arxiv.org/abs/2605.20695)) · 사이클 이중 덮개 해설(Geelen, [arXiv 2607.15399](https://arxiv.org/abs/2607.15399); 엄상일, [arXiv 2607.16356](https://arxiv.org/abs/2607.16356)) · 나비에-스토크스([Scientific American, 2026-09-21](https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/), [Quanta](https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/)) · [OpenAI 수학 원고 저장소](https://github.com/openai/math) · 7/8 경계를 이은 논문(Liu, [arXiv 2610.12234](https://arxiv.org/abs/2610.12234)) · 필즈상 수상자 성명 보도([TechCrunch](https://techcrunch.com/2026/09/11/openais-feud-with-mathematicians-is-only-escalating/))
- 국내 보도 예: [SBS Biz](https://biz.sbs.co.kr/amp/article/20000334030) · [파이낸스스코프(2026-10-08)](https://www.finance-scope.com/article/view/scp202610080003) · [여성경제신문(2026-05-03, 다음)](https://v.daum.net/v/20260503181120270) · [뉴시스(2026-09-12)](https://newsis.com/view/NISX20260912_0003786891)
- 증명 채점: Proof or Bluff([arXiv 2503.21934](https://arxiv.org/abs/2503.21934))
- 시험 수학 AI: 풀이 과정([arXiv 2201.11903](https://arxiv.org/abs/2201.11903)) · 다수결([arXiv 2203.11171](https://arxiv.org/abs/2203.11171)) · 도구 사용 PAL([arXiv 2211.10435](https://arxiv.org/abs/2211.10435))·ToRA([arXiv 2309.17452](https://arxiv.org/abs/2309.17452)) · 단계 채점([arXiv 2305.20050](https://arxiv.org/abs/2305.20050)) · DeepSeek-R1([arXiv 2501.12948](https://arxiv.org/abs/2501.12948)) · GSM-Symbolic([arXiv 2410.05229](https://arxiv.org/abs/2410.05229)) · 콴다 인터뷰([바이라인네트워크, 2021](https://byline.network/2021/03/22-121/))
- 수능: [연합뉴스 팩트체크(2025-11-15, 다음)](https://v.daum.net/v/20251115070121527) · KCSAT-ML([arXiv 2606.10403](https://arxiv.org/abs/2606.10403))
- 엔진: [SymPy](https://www.sympy.org) · [Pyodide](https://pyodide.org) · 수식 표시 [KaTeX](https://katex.org)