수학의 미래는 대단히 기묘할지도 모릅니다
소설 속에서 수학자는 흔히 고독한 인물로 그려집니다. 난해한 기호가 빽빽한 칠판 앞에서 깊은 집중에 빠진 채 자기만의 세계에 갇힌 인물입니다. 과거에는 그런 모습에 어느 정도 진실이 담겨 있었을지도 모르지만, 오늘날 수학은 훨씬 더 사회적인 현상입니다. 미래의 수학자들은 페르마의 마지막 정리를 증명하려고 10년 동안 홀로 매달린 앤드루 와일스 같은 천재의 전형보다는, Github에서 풀 리퀘스트와 씨름하는 소프트웨어 엔지니어와 훨씬 더 많은 공통점을 지니게 될지도 모릅니다.
자동 정리 증명은 수학적 증명을 자동으로 구성하거나 사람이 작성한 증명이 올바른지 검증할 수 있는 소프트웨어 시스템을 개발하는 컴퓨터 과학 분야입니다. 이러한 시스템은 형식 논리, 타입 시스템, 기호 추론을 사용하여 수학적 논증의 각 단계가 앞선 단계와 확립된 공리로부터 논리적으로 도출되는지 확인합니다. 자동 정리 증명기는 수학적 지식을 정밀하고 기계가 읽을 수 있는 형식으로 인코딩함으로써 인간의 오류를 없애고 수학적 결과의 타당성을 절대적으로 보장할 수 있습니다.
정리 증명 생태계를 잘 모르는 분들을 위해 설명하자면, (Lean4, Coq, 그리고 그 선배 격인 Isabelle, Agda, HOL4 등) 한때 컴퓨터 과학 연구의 난해한 최전선에만 머물던 이 도구들이 이제 수학의 실천과 철학 자체를 재편하려 하고 있습니다. 이 학문의 미래는 우리가 지금 상상할 수 있는 것보다 훨씬 더 기묘하고, 더 협업적일 수 있습니다. 게다가 언어 모델이 동시에 등장하면서, 그 미래는 우리가 지금 상상할 수 있는 것보다 훨씬 더 흥미롭고 빠르게 다가올 수도 있습니다.
아래는 소수가 무한히 많다는 유클리드 정리를 Lean으로 형식화한 것입니다. 이 증명은 유클리드의 구성적 접근을 따릅니다. 임의의 자연수 n이 주어지면 n! + 1의 가장 작은 소인수를 고려하여 소수 p ≥ n을 구성합니다. 이 Lean 증명은 여러 택틱과 보조정리를 사용합니다. minFac은 최소 소인수를 찾고, factorial_pos는 계승이 양수임을 보이며, minFac_prime은 최소 인수가 실제로 소수임을 증명하고, dvd_factorial은 나누어떨어짐 성질을 다룹니다. Nat.dvd_add_iff_right를 통해 형식화된 핵심 통찰은, 어떤 소수가 n!과 n! + 1을 모두 나눈다면 그 차(즉 1)도 나누어야 한다는 것이며, 소수는 1을 나눌 수 없으므로 모순에 이르게 됩니다. 이것은 모든 수학과 학부생이 1학년 때 배우는 증명입니다.
/-- Euclid's theorem on the **infinitude of primes**.
Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/
theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=
let p := minFac (n ! + 1)
have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
have pp : Prime p := minFac_prime f1
have np : n ≤ p :=
le_of_not_ge fun h =>
have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
pp.not_dvd_one h₂
⟨p, np, pp⟩
표준 학부 수학 교육과정을 이와 같은 형식으로 형식화하는 일은 더 이상 먼 꿈이 아닙니다. 그것은 가까운 시일 안에 달성할 수 있는 목표입니다. 표준 라이브러리인 Mathlib을 살펴보기만 해도, 표준 정리들에 대한 진척이 이제 놀라울 만큼 방대하고 표현력이 풍부하다는 것을 알 수 있습니다. 이러한 진척을 보여 주는 또 다른 좋은 예는 테렌스 타오의 교과서 Analysis I의 형식화입니다. 이 교과서는 탐색할 수 있고 상호 연결되어 있으며 기계로 검증할 수 있는 정리 모음으로 꼼꼼하게 옮겨졌습니다. 모든 교과서에 디지털 대응물이 있고, 어떤 정리나 보조정리든 “더블 클릭”하여 그 맥락과 정의를 펼쳐 볼 수 있는 미래는 이제 더 이상 공상 과학이 아닙니다. 사실상 이미 와 있습니다.
Lean을 직접 실험해 보고 싶다면 다음 단계를 따라 아주 빠르게 시작할 수 있습니다.
- Visual Studio Code(비주얼 스튜디오 코드)를 설치하십시오.
- Lean + Elan을 설치하십시오.
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
elan default leanprover/lean4:stable
- Lean 4 VS Code(VS 코드) 확장을 설치하십시오: VS Code를 열고 → Extensions → Lean 4를 검색하십시오(작성자:
leanprover.lean4) - 새 Lean 프로젝트를 초기화하십시오.
lake init my_project
cd my_project
lake build
Lean 생태계에는 오픈 소스 도구들도 활발하게 늘어나고 있습니다. Mathlib 라이브러리는 형식화된 수학을 모아 둔 거대한 협업 저장소로, 날마다 성장하고 있습니다. 이 방대한 디지털 라이브러리를 탐색할 수 있도록 여러 검색 엔진이 등장했습니다. Moogle은 시맨틱 검색을 제공하여 정확한 표현이 아니라 개념적 의미를 바탕으로 정리를 찾을 수 있게 해 줍니다. Loogle은 특정 논리 구조와 일치하는 표현식을 찾는 데 특화되어 있으며, LeanSearch는 자연어 질의를 지원합니다. 실험해 보고 싶은 분들을 위해 Lean 4 Playground는 웹 브라우저에서 바로 증명을 작성하고 검사할 수 있는 대화형 환경을 제공합니다.
이것이 가능하게 할 교육 환경을 생각해 보십시오. 모든 수학과 1학년 학생이 자기 전공 분야의 검증된 기초 전체를 담은 200메가바이트짜리 파일 하나를 내려받는 미래를 상상해 보십시오. 학생들은 LLM 기반 튜터의 안내를 받게 됩니다. 이 튜터는 수업을 계획하고, 복잡한 증명을 말로 풀어 설명하며, 학생이 직접 시도한 증명에 대해 정리 증명기로 검사할 수 있는 피드백을 즉시 제공합니다. 이것은 공상 과학이 아닙니다. 교육과정을 계획하고 자연어로 설명하는 기술은 오늘날 이미 대부분 우리 손이 닿는 곳에 있습니다. 물론 이러한 전망은 현실적인 시각으로 다듬어야 합니다. 과학은 본질적으로 사회적 현상입니다. 수학 연구의 상당 부분은 안목을 기르는 일, 곧 무엇이 우아한 증명인지 알아보는 미적 감각과 어떤 문제가 추구할 가치가 있는지 가늠하는 직관을 기르는 일입니다. 이것들은 문화와 협업에서 생겨나는 이 분야의 무형적 자질이며, 기계는 이를 끝내 온전히 포착하지 못할 수도 있습니다.
확립된 지식에서 열린 연구의 최전선으로 나아갈수록 이 도구들은 새롭고 흥미로운 가능성을 보여 줍니다. 형식화된 증명은 점점 늘어나고 있지만, 형식화된 미해결 추측은 아직 상대적으로 부족합니다. Deepmind의 형식 추측 색인 같은 프로젝트는 여러 가지 이유로 가치가 있습니다. 첫째, AI 기반 자동 정리 증명기 개발을 위한 명확하고 도전적인 벤치마크 모음을 제공합니다. 둘째, 형식화하는 행위 자체가 수학자로 하여금 추측의 정확하고 모호하지 않은 의미를 분명히 하도록 강제합니다. 기계가 만들어 내는 수학의 경계를 체계적으로 넓히려는 시도로, 일종의 차세대 AlphaGeometry라 할 강력한 신경기호(neurosymbolic) 시스템이 이 목록에 투입되는 모습을 머지않아 보게 될 것이 거의 확실합니다.
이러한 연구가 만들어 내는 산출물은 그 자체로 깊이 있는 연구의 대상이 될 것입니다. 정리 증명기의 피드백을 보상 함수로 삼아 강화 학습으로 훈련되어 학부 수학 전체를 통달한 신경망의 20기가바이트짜리 가중치를 누구나 내려받을 수 있는 미래를 그려 보십시오. 그러한 모델이 존재한다면 흥미로운 이론적, 철학적 질문들이 제기될 것입니다. 같은 결과를 낼 수 있는, 더 작고 더 우아한 모델이 있을까요? 그 모델이 실패하는 방식을 살펴봄으로써 수학의 복잡도 장벽에 대해 무엇을 배울 수 있을까요? 그 모델은 다른 공리계를 어떻게 다룰 것이며, 어떤 문제가 주어진 공리와 근본적으로 독립적인지를 직관적으로 알아채는 식으로 괴델의 불완전성을 “이해“하게 될 수 있을까요? “스스로” 수학을 할 수 있는 거대하고 불가해한 행렬이 존재한다는 증명을 손에 넣는다면, 우리가 던질 수 있는 깊은 메타수학적 질문은 무수히 많습니다. 그런 것이 존재할 수 있다는 보장은 없지만(그리고 괴델, 튜링, 힐베르트 프로그램에 관한 통상적인 분석은 여전히 유효하지만), 만약 존재할 수 있다면 — 제한적으로나마 — 완전히 새로운 질문의 세계가 열립니다.
상상력을 더 넓혀 보면, 이 기술이 정점에 이르는 먼 미래를 그려 볼 수 있습니다. 전용 데이터 센터에 리만 가설 같은 거대한 난제를 맡길 수도 있습니다. 몇 주간의 연산 끝에 데이터 센터는 긍정적인 결과, 즉 기계로 검사할 수 있는 완전한 증명을 내놓을지도 모릅니다. 그러나 그 증명의 내부 구조는 너무나 복잡하고 논리가 너무나 낯설어서, 컴퓨터를 이용한 4색 정리의 증명이나 ABC 추측에 대한 모치즈키의 증명을 둘러싼 논란처럼, 어떤 인간도 그 직관적 요지를 파악하기를 기대할 수 없을지도 모릅니다. 이는 불안한 새 현실을 불러올 것입니다. 이언 M. 뱅크스의 컬처 시리즈에 나오는 초지능 마인드처럼 기계가 인간의 이해를 영원히 넘어서는 지적 영역으로 나아가는 세계입니다. 우리는 (인식론적 문제는 제쳐 두고) 어떤 수학적 진리를 “알고” 받아들이겠지만, 인간으로서 그것이 왜 참인지는 결코 직관하거나 이해하지 못할 것입니다. 그리고 그것은 과학이 이루어지는 방식이 전혀 다른 세계입니다.
기계가 생성한 불가해한 증명이라는 전망은 지식과 이해의 본질에 관한 근본적인 질문과 맞닿아 있습니다. 빌 서스턴은 자신의 에세이 “On Proof and Progress in Mathematics,”에서 이러한 긴장을 다음과 같이 포착했습니다.
컴퓨터의 급속한 발전은 이 점을 더욱 극적으로 드러내는 데 기여했습니다. 컴퓨터와 사람은 매우 다르기 때문입니다. 예를 들어, 아펠(Appel)과 하켄(Haken)이 대규모 자동 계산을 이용해 4색 지도 정리의 증명을 완성했을 때, 이는 많은 논란을 불러일으켰습니다. 저는 그 논란이 정리의 진실성이나 증명의 정확성에 대해 사람들이 품은 의심과는 거의 관계가 없었다고 해석합니다. 오히려 그 논란은 정리가 참이라는 사실을 아는 것에 더해, 증명을 인간이 이해하고자 하는 변함없는 열망을 반영한 것이었습니다.
새로운 발전은 수학이라는 학문의 목적 그 자체에 대한 목적론적 질문도 제기합니다. 수학은 결코 참인 명제를 축적하는 것만이 전부였던 적이 없습니다. 수학은 통찰을 키우고, 직관을 쌓고, 실재의 근본 구조를 밝혀 주는 틀을 만들어 가는 일입니다. 발견의 과정, 이해에 이르는 “아하!“의 순간, 서로 무관해 보이는 분야들 사이의 우아한 연결. 이러한 것들이 수학을 하는 사람들에게 수학을 의미 있게 만드는 것의 상당 부분을 이룹니다. 파인만이 언젠가 말했듯이 말입니다. “물리학은 섹스와 같습니다. 물론 실용적인 결과를 낼 수도 있지만, 우리가 그것을 하는 이유는 그 때문이 아닙니다.”
솔직히 말해, 이런 전망 앞에서 감정적이 되지 않기란 어렵습니다. 그런 미래에서도 우리 중 많은 이들은 여전히 정리가 왜 참인지 알아내는 일에 깊은 관심을 가질 것입니다. 그러한 질문에 답해 가는 과정은 지적 삶에서 가장 아름답고 충만한 측면 중 하나입니다. 하나의 실천으로서의 수학은 우주적인 할 일 목록에서 정리를 하나씩 지워 나가는 일 이상의 것입니다. 하지만 이 전제를 받아들이고, 여러분이 떠오르는 모델 설계자라면, 노벨상(그리고 다른 여러 상)을 받기 위해 여러분이 할 일은 Lean 정리가 여러분의 답을 검증하도록 다음 개의 토큰을 자동 완성하게끔 여러분의 확률적 앵무새를 훈련시키는 것뿐입니다.
theorem infinite_irrational_at_odd :
{ n : ℕ | ∃ x, Irrational x ∧ riemannZeta (2 * n + 1) = x }.Infinite := by
...
그 과정에서 밀레니엄 재단으로부터 무려 백만 달러도 손에 넣게 될 것이며, 이는 여러분의 GPU 청구서의 1/100 정도는 충당해 줄지도 모릅니다. 아니면 그냥 AI 슬롭판 무한한 재미(Infinite Jest) 버전의 틱톡을 만드는 편이 나을 수도 있습니다. 안타깝게도 그쪽이 리만 가설을 풀고 인류 지식의 지평을 넓히는 것보다 단기 투자 수익률 면에서 훨씬 나을 가능성이 높기 때문입니다.
하지만 농담은 제쳐 두고, 우리는 아직 그 단계에 이르지 못했습니다. 근처에도 가지 못했습니다. Terence Tao가 Claude 및 o4와 함께 Lean 정리 증명을 시도한 최근 유튜브 스트림을 보기만 해도, 현재 시스템이 중간 정도로만 어려운 수학 문제를 마주해도 뚜렷한 한계를 드러낸다는 것을 알 수 있습니다. 모델들은 기본적인 증명 전략에도 어려움을 겪고, 초보적인 논리 오류를 저지르며, 문법적으로는 올바르지만 수학적으로는 무의미한 Lean 코드를 자주 만들어 냅니다. 그러나 이러한 실험이 펼쳐지는 것을 지켜보면, 이 지형이 얼마나 빠르게 바뀔 수 있을지 그려 보는 데 대단한 상상력의 도약이 필요하지는 않습니다. 점점 더 정교해지는 언어 모델, 정리 증명기와의 향상된 통합, 그리고 형식적 수학 추론을 위해 특별히 설계된 더 나은 훈련 방법론의 결합은, 오늘날의 서투른 첫 시도들이 진정으로 더 유능한 모델들에게 자리를 내줄 수 있음을 시사합니다. 하지만 물론 진보는 결코 확실하지 않습니다. 극복해야 할 장애물이 훨씬 더 많을 수도 있습니다.
이러한 전망은 수학에서 인간적 요소를 약화시키는 것처럼 보일 수 있지만, 어쩌면 그러한 우려는 근거가 없는 것일지도 모릅니다. 컴퓨터는 체스와 바둑이라는 게임을 결정적으로 정복했습니다. Stockfish와 AlphaGo는 지구상의 어떤 인간 플레이어라도 손쉽게 이길 수 있습니다. 그럼에도 체스는 그 어느 때보다 인기가 많습니다. 이 강력한 시스템들은 게임을 죽이지 않았습니다. 오히려 훈련, 분석, 감상에 없어서는 안 될 도구가 되어, 그 어느 때보다 더 많은 사람이 게임에 더 쉽게 다가갈 수 있게 해 주었습니다. 수학에서도 마찬가지일 가능성이 있습니다. 이 낯설고 강력한 새로운 도구들이 확산되더라도, 인간 수학자를 쓸모없게 만들지는 않을 수 있습니다. 오히려 이 도구들은 수학적 추론에 대한 접근을 민주화하여, 더 많은 사람이 가장 오래되고 가장 추상적인 학문에 참여할 수 있게 할지도 모릅니다. 어쩌면 지식의 최전선은 놀라운 속도로 넓어지겠지만, 그 최전선에 이르는 길은 모든 사람에게 더 열려 있을 것입니다. 그리고 어쩌면 그것이야말로 정말로 밝은 미래일 것입니다.