2026년 7월 20일, 임페리얼 칼리지 런던의 수학과 교수 Kevin Buzzard는 동료들에게 따가운 일침을 가하는 글을 블로그에 올렸다: 인간 수학자들이 ‘반례 초월’을 당하고 있다. 이유는 AI가 단 두 달 만에 수십 년간 풀리지 않던 세 가지 수학 추측을 연속으로 무너뜨렸기 때문이다. 그중 하나는 거의 한 세기 가까이 미해결 상태였다.
Buzzard는 직접 이렇게 말했다: 「60년 동안 풀리지 않았던 대수기하학 반례를 확인하는 데 5분도 채 걸리지 않았다. Lean 코드를 노트북에 내려받고 컴파일을 통과시킨 다음, 고개를 끄덩이며 ‘그래, 이건 정말 반례군’이라고 말했을 뿐이다.」
5분. 이것이 인간 수학과 AI 수학의 경계선이다. 오늘 이 글에서 이야기하려는 것은, 이 경계선이 언제 그어졌는지, 그리고 그것이 무엇을 의미하는지다.
반례: 증명보다 날카로운 칼
먼저 기본 개념부터 짚어보자. 수학에서 어떤 명제가 참임을 증명하는 것은 매우 어렵다 — 매 단계마다 오류가 없는 엄밀한 추론을 전개해야 하기 때문이다. 하지만 명제가 거짓임을 증명하는 것은 상대적으로 「간단」하다: 모든 전제 조건을 만족하면서 결론을 충족하지 않는 구체적인 구축물, 즉 반례 하나만 찾으면 된다.
누군가 「모든 백조는 흰색이다」라고 말한다면, 전 세계의 모든 백조를 조사할 필요 없이 검은 백조 한 마리만 찾으면 된다.
하나의 반례는 한 수학자의 평생 연구를 종식시킬 수 있다. 그렇기 때문에 반례는 수학사에서 창조적인 역할을 해왔다 — 이론의 경계가 어디인지 드러내고, 수학자들로 하여금 가정을 재검토하고 정의를 개선하며 이론을 발전시키도록 강제한다. 어떤 관점에서 보면, 반례야말로 수학 발전의 연료다.
AI는 지금 이 「검은 백조 찾기」 기술을 상상할 수 없는 규모로 끌어올리고 있다.
2026년 5월~7월: AI의 3연타
지난 석 달 동안 무슨 일이 있었는지 시간순으로 정리해보자.
첫 번째 타격: 에르되시 단위 거리 추측 (1946년 제기, 2026년 5월 20일 붕괴)
전설적인 수학자 Paul Erdős가 1946년에 제기한 이산기하학 문제. ChatGPT가 반례 구성을 제시했다. Buzzard의 첫 반응은 「Lean으로 검증했나?」였다. 아니었다. 그러나 일주일도 채 지나지 않아 필즈상 수상자 Mike Freedman(현 AI 회사 Logical Intelligence의 최고과학책임자)이 메일을 보내왔다 — 그들의 시스템이 이 논증을 자동으로 Lean 코드로 번역했다는 소식이었다.
한 달 후, OpenAI의 Boris Alexeev가 새 모델 Sol로 더 철저한 작업을 완료했다: 수학 공리에서 출발해 반례 전체를 완전히 형식화한 것이다. Sol은 이를 위해 120만 줄의 Lean 코드를 생성했다.
비교해보자: Lean 커뮤니티가 9년에 걸쳐 작성한 핵심 수학 라이브러리 mathlib의 전체 코드는 230만 줄이다. AI가 3주 만에 생성한 양이 인간이 9년 동안 쌓아온 것의 절반에 육박한다. Buzzard의 평은 간단했다: 「대규모 AI 생성 수학의 발전은 이미 불가피해졌다.」
두 번째 타격: 그로텐디크 군 스킴 문제 (1960년대 제기, 2026년 7월 11일 붕괴)
Grothendieck은 20세기 가장 위대한 수학자 중 한 명이다. 60년 전 그는 한 가지 질문을 던졌다: n차 유한 자유군 스킴(finite free group scheme of order n)은 반드시 n에 의해 소멸(annihilated)되는가? Deligne은 교환(commutative) 경우가 성립함을 증명했고, Grothendieck 자신은 밑환(base ring)이 기약(reduced)인 경우가 성립함을 증명했다 — 하지만 완전한 결론은 미궁에 남아 있었다.
Sol이 반례를 찾았다. 전체 증명은 단 1076줄의 Lean 코드였다. Buzzard는 5분도 안 되어 모든 검증을 통과시켰다. 그는 수학자 Akhil Mathew에게 이 반례를 수학 라이브러리에 제출할 것을 권하면서 농담을 던졌다: 「다음 번에는 Hodge 추측에 도전해보는 게 어때?」
세 번째 타격: 야코비안 추측 (1939년 제기, 2026년 7월 19일 붕괴)
이것이 가장 충격적이다. 야코비안 추측(Jacobian Conjecture)은 다항식 사상의 역문제다: 어떤 다항식 사상의 야코비안 행렬식이 0이 아닌 상수라면, 그 사상은 반드시 가역(invertible)일까? 이 문제는 1939년부터 지금까지 미해결 상태로 남아 있었으며, 대수기하학에서 가장 매혹적이면서도 가장 완고한 추측 중 하나로 불려왔다.
이번에는 Anthropic의 Claude Fable이 나섰다. Fable은 2026년 월드컵 결승전 기간 중에 반례를 찾았다. 다음날, 테렌스 타오(Terence Tao) — 현대 수학계에서 가장 존경받는 인물 중 한 명 — 가 이 반례의 수학적 의미를 상세히 「소화」하는 블로그 글을 발행했다.
타오의 계산에 따르면, 이 반례는 세 변수를 가진 최고 7차 다항식 사상이다. 야코비안 행렬식은 -2 — 즉 0이 아닌 상수 조건을 만족한다 — 하지만 이 사상은 세 개의 서로 다른 입력점을 동일한 출력점으로 매핑하므로 일대일 대응이 아니며, 따라서 가역적이지 않다. 더욱 놀라운 점은, AI가 120개의 조정 가능한 매개변수를 사용해 야코비안 행렬식에 이론적으로 나타날 수 있는 1329개 항의 계수를 제어하여, 0이 아닌 모든 항이 정확히 상쇄되도록 했다는 것이다. 타오의 표현을 빌리자면: 「이것은 거대한 기적처럼 보인다.」
Lean + LLM: 창의성과 확실한 증명의 결혼
이야기를 마쳤으니, 이제 기술적 논리를 정리해보자.
Lean은 일종의 「수학 컴파일러」다. Lean으로 수학 증명을 작성하면, 모든 추론 단계가 엄격한 타입 검사를 통과해야 한다. 「자명한 단계는 생략한다」는 없다 — 모든 「자명함」은 원자 수준까지 전개되어야 한다. 코드가 컴파일을 통과하면, 그 증명은 수학적으로 절대적으로 올바른 것이다 — 어떤 인간 심판의 신뢰에도 의존하지 않는다.
LLM(대규모 언어 모델)은 「구상」을 담당하고, Lean은 「심판」을 담당한다. LLM이 수학을 다룰 때의 고질적인 약점은 헛소리를 한다는 점이다 — 실제로 알지 못하면서도 그럴듯한 추론을 지어낸다. Lean의 개입은 이 문제를 근본적으로 해결한다: LLM이 Lean 코드를 생성하면 컴파일러가 즉시 검사한다. 컴파일이 실패하면 LLM은 오류 메시지를 받고 수정한다. 이 과정을 반복해 코드가 컴파일을 통과할 때까지 — 이 단계에 도달하면 AI가 생성한 수학 결과는 엄격한 정확성을 보장받는다.
2026년 3월, 『Learning to Disprove』라는 제목의 논문이 이 방법론을 체계적으로 제시했다. 핵심 통찰은 이것이다: LLM에게 명제를 「증명」하라고 시키는 대신(헛소리를 할 위험이 큼), 「반례를 찾도록」 하는 것이 낫다 — 반례는 일단 Lean으로 컴파일되면 확실한 증거가 되기 때문이다. 논문 저자들은 「기호 변형(symbolic variation)」 전략을 채택해, 기존 정리에서 특정 조건을 체계적으로 제거함으로써 반례 탐색이 필요한 대량의 학습 데이터를 생성하고, 다중 보상 메커니즘으로 LLM을 훈련시켰다. 실험 결과, 반례 생성 과제에서 LLM의 정확도가 49% 향상되었다.
이것이 「반례 초월」의 기술적 기초다: LLM이 창의성을, Lean이 확실한 증거를 담당하고, 인간 수학자는 관객이 되었다 — 적어도 결과 검증 단계에서는.
수학계의 「슬픔의 5단계」
Buzzard는 블로그 글에서 주변 수학자들의 반응을 솔직하게 기록했다. 임페리얼 칼리지의 점심시간에 동료로부터 이런 말을 들었다: 「반례를 이렇게 쉽게 찾을 수 있다는 것은, 인간이 이 문제에 충분한 시간을 투자하지 않았다는 증거일 뿐이다.」 그는 속으로 씁쓸한 웃음을 지었다 — 자신도 한때 이 「투자할 가치가 없는」 문제에 꼬박 일주일을 쏟아부었기 때문이다.
이는 전형적인 부정(denial) 단계다.
그 다음은 흥정(bargaining)이었다. 한 교수는 놀라움을 담은 이메일을 보냈다: 왜 대학원생들이 매월 200달러를 내며 Sol과 Fable을 구독하는지 이해할 수 없다는 내용이었다. Buzzard의 답변은 직설적이었다: 「200달러를 내지 않는 박사과정생이야말로 비합리적이다.」 하버드대학교는 이미 모든 수학 박사과정생, 박사후연구원, 교수진에게 Fable 사용 권한을 무료로 제공하고 있다.
감정적으로 받아들이든 말든, 한 가지 사실은 명확하다: 수학 연구에서 AI 도구를 사용하는 사람과 사용하지 않는 사람 사이의 능력 격차는 달 단위로 벌어지고 있다.
테렌스 타오가 제시한 방향
모든 응답 중에서 테렌스 타오의 태도가 가장 주목할 만하다. 그는 AI의 능력 한계에 의문을 제기하지도 않았고, 「이것이 여전히 수학인가」라는 철학적 논쟁에 빠지지도 않았다. 그는 앉아서 상세한 블로그 글을 작성했고, 다항식의 가중 준동차성(weighted homogeneity)을 계산했으며, 기하학적 관점에서의 재구성을 제시했고, GPT-5와의 대화 기록 전체를 공개하기까지 했다.
이것은 전형적인 현장 수학자의 태도다: 결과가 나와 있으면, 먼저 이해하고, 그 다음 활용한다.
타오는 HN 토론에서 이렇게 지적했다: 「이 사건은 우리에게, 겉보기에는 불가능해 보이는 수학적 구성도 충분히 큰 탐색 공간 안에서는 발견될 수 있다는 것을 보여준다.」 이 문장의 숨겨진 핵심 메시지는 이것이다 — 탐색 공간은 거대하지만, AI가 우리에게 탐색 방법을 가르쳐주었다. 그리고 이것은 시작에 불과하다.
수학자에게 남은 것은 무엇인가?
AI가 반례를 찾고, 증명을 검증하고, 완전한 이론을 자동으로 형식화할 수 있다면, 수학자에게 남은 것은 무엇일까?
Buzzard가 내놓은 답은 이것이다: 이해와 설명. 그는 말한다: 「이 비범한 예시들의 진정한 가치는, 인간에게 수학에 대한 더 깊은 이해를 제공한다는 점에 있다.」 Akhil Mathew는 이미 그로텐디크 반례의 이면에 있는 구조를 더 깊은 관점에서 이해하려 시도하고 있다 — 「여기서 실제로 무슨 일이 일어나고 있는가」를추궁하며, 단순히 「우연한 구성과 계산의 일치」에 머물지 않는다.
AI는 「그것은 성립하지 않는다」고 말할 수 있지만, 「이것이 우리의 수학적 그림에 무엇을 의미하는가」를 설명하지는 못하는 경우가 많다.
역사적으로 수학자들은 계속해서 「계산」을 기계에 아웃소싱한 다음, 더 높은 수준의 「이해」와 「구성」에 집중해왔다. 이제 「반례 찾기」와 「증명 검증」도 아웃소싱할 수 있게 되었다. 남은 인간의 작업은 아마도 수학에서 가장 핵심적인 부분일 것이다: 기계가 반례를 테이블 위에 올려놓았을 때, 그것이 왜 의미 있는지 진정으로 이해하고 — 그리고 그로부터 무엇을 배울 수 있는지를 깨닫는 것.
이것은 수학의 종말이 아니다. 그러나 수학자의 역할은, 분명히 돌이킬 수 없는 진화를 겪고 있다.
참고 링크:
- Xenaproject — Kevin Buzzard의 원본 블로그 글 「인간 수학자들이 반례 초월을 당하고 있다」
- HN 토론 (id: 48998362) — 테렌스 타오의 야코비안 추측 블로그를 둘러싼 커뮤니티 토론
- Lobsters 토론 (s/wfmpqr) — 기술 커뮤니티의 AI 수학 반례에 대한 심층 논평
- Terry Tao의 블로그 글 — 야코비안 추측 반례의 소화와 수학적 재구성
- SBSeminar — 야코비안 추측 새 반례의 수학적 세부 논의
- arXiv 2603.19514 — Learning to Disprove: 대규모 언어 모델을 활용한 형식적 반례 생성
- New Scientist 잡지 보도 — AI의 87년 수학 난제 해결
- GitHub DeepMind Formal Conjectures — 형식화 추측 저장소, 야코비안 반례 포함
