현대 수학 연구에서의 추상화

by I Seul Bee

9부의 말미에서 예고한 대로, 이제 정형화된 강의실을 벗어나 역동적인 연구의 현장으로 시선을 옮겨 보자. 지금까지 우리는 군, 벡터공간, 위상공간, 측도공간이라는 이미 정리된 추상적 결과물들이 역사적으로 어떻게 형성되었으며 오늘날 학생들에게 어떻게 전달되는지를 살펴보았다. 그런데 새로운 정리를 증명해야 하는 현역 수학자 앞에는 매 순간 비슷한 딜레마가 놓인다. 눈앞의 문제를 과연 얼마나 일반적이고 추상적인 언어로 공략할 것인가? 문제에 지나치게 구체적으로 다가가면 비슷한 문제를 만날 때마다 증명을 처음부터 다시 전개해야 할 수 있다. 반대로 지나치게 일반적인 틀을 먼저 세우면, 눈앞의 문제가 지닌 고유한 핵심이 불필요한 장치 속에 가려질 수 있다. 이러한 판단은 하나의 공식으로 정리하기 어렵지만, 연구자가 정리의 가정과 언어를 설계할 때 거듭 마주하는 실무적 문제다.

가워스의 두 문화

필즈상 수상자인 영국의 수학자 티모시 가워스(Timothy Gowers)는 2000년에 발표한 에세이 「수학의 두 문화(The Two Cultures of Mathematics)」에서 순수수학 내부의 두 연구 성향을 구분했다.[Gowers2000]

[이 제목은 영국의 과학자이자 소설가 C. P. 스노(C. P. Snow)가 1959년 리드 강연 「두 문화와 과학혁명(The Two Cultures and the Scientific Revolution)」에서 과학과 인문학 사이의 단절을 논한 데서 의식적으로 가져온 것이다. 가워스는 글 첫머리에서 이 연원을 직접 밝힌다.[Snow1959]]

가워스가 구분한 두 성향은 이론 구축가(theory-builder)와 문제 해결사(problem-solver)이다. 이론 구축가는 여러 현상을 조직하는 개념과 구조를 만들고 이해하는 일을 중시한다. 반면 문제 해결사는 구체적인 문제에서 출발하여 그 문제를 돌파할 논증과 기법을 찾는 일을 중시한다. 대부분의 수학자는 두 활동을 모두 하며, 수학은 두 성향을 모두 필요로 한다.[Gowers2000]

이론 구축형 연구에서는 하나의 적절한 구조를 세움으로써 그 공리를 만족하는 여러 사례를 한꺼번에 다룰 수 있다. 이 연재에서 살펴본 군, 위상공간, 측도공간의 공리화가 그러한 힘을 보여 준다. 문제 해결형 연구에서는 반대로 구체적인 문제의 조합적 배치나 수치적 제약처럼 일반 이론이 즉시 포착하지 못하는 특징을 깊이 파고든다. 가워스의 핵심 주장 가운데 하나는 조합론에도 구조와 축적이 있으며, 그 조직 원리가 거대한 이론의 형태보다 확률적 방법, 준무작위성, 집중 현상 같은 널리 쓰이는 일반 원리의 형태로 덜 명시적으로 나타날 수 있다는 것이다.[Gowers2000]

가워스는 조합론을 문제 해결사 문화가 강하게 나타나는 분야로 논하면서, 조합론이 이론 구축형 분야보다 얕거나 주변적이라는 평가에 맞섰다. 그는 정리들 사이에 긴 형식적 의존 사슬이 보이지 않더라도, 한 증명에서 발전한 일반 원리가 다음 세대의 문제 해결을 가능하게 하는 또 다른 종류의 의존 관계가 있다고 설명한다. 문제 해결형 수학에도 고유한 깊이와 전승 방식이 있음을 인정하고 두 문화 사이의 교류를 넓히자는 것이다.

[가워스는 실제로 램지 정리와 램지 수 \(R(k)\)의 상·하한 문제를 중심 사례로 든다. 특히 더 나은 상한은 그 문제에만 맞춘 임시 논증보다 중요한 새 기법을 요구할 가능성이 크다고 보았다. 이 사례의 요지는 램지 이론 전체가 구조 이론과 무관하다는 것이 아니라, 조합론의 일반 원리가 때로 개별 문제의 증명 속에 덜 명시적으로 축적된다는 데 있다.[Gowers2000]]

아놀드, 형식주의를 겨누다

러시아의 수학자 블라디미르 아놀드(Vladimir Arnol'd)는 1997년 3월 7일 파리 팔레 드 라 데쿠베르트(Palais de la Découverte)에서 한 강연을 확장한 글에서, 수학 교육이 물리적 동기와 기하학적 직관에서 멀어지고 형식적 정의와 증명만을 앞세우는 경향을 격렬하게 비판했다. 이 글은 1998년 「On Teaching Mathematics」라는 제목으로 출판되었다.[Arnold1998]

[“Mathematics is a part of physics”는 이 글의 출판 제목이 아니라 첫 문장이자 아놀드의 핵심 명제다. 정확한 문헌명은 「On Teaching Mathematics」이며, 영어 번역은 1998년 Russian Mathematical Surveys 53권 1호에 실렸다.[Arnold1998]]

아놀드의 관점에서 수학은 공간, 운동, 힘과 같은 구체적 현상을 탐구하는 과정에서 자라났고, 계산과 그림과 실험적 유비는 정리를 발견하는 중요한 통로다. 그는 특히 부르바키로 상징되는 탈기하학적·공리주의적 교육이 이러한 통로를 차단한다고 주장했다. [같은 글에서 아놀드는 프랑스 초등학생과 대학생에 관한 일화, 그리고 ENS 학생들이 포물면이나 매개변수 곡선을 다루는 데 어려움을 겪었다는 자신의 교육 경험을 들었다.]

이 비판은 9부에서 다루었던 새수학(New Math)의 일부 형식주의적 흐름과 접점을 갖는다. 부르바키의 구조 개념이 연구수학에서 발휘한 통합의 힘과, 고도로 추상적인 개념을 학교 교육에 옮길 때 생긴 교수학적 문제는 서로 다른 층위의 쟁점이다. 더구나 ‘새수학’은 여러 나라에서 전개된 다양한 개혁을 묶어 부르는 말이지 하나의 단일한 프로그램이 아니었다.

추상화의 옹호자들은 반대편의 사례를 제시할 수 있다. 19세기 말 파슈와 힐베르트 등의 공리적 연구는 유클리드 기하학에서 암묵적으로 사용되던 전제를 드러내고 기하학의 논리적 구조를 재정비했다. 군의 추상적 언어는 방정식론을 넘어 결정학과 양자역학을 포함한 여러 분야의 대칭을 표현하는 도구가 되었다. 그로텐디크와 공동 연구자들이 발전시킨 스킴과 에탈 코호몰로지의 틀은 베유 추측의 앞부분을 증명하고 마지막 추측을 향한 기반을 제공했으며, 마지막 핵심인 유한체 위 대수다양체의 리만 가설은 1974년 피에르 들리뉴가 증명했다.

적정 일반성

이 철학적 논쟁을 실무의 언어로 옮기면 “방금 얻은 정리를 어느 수준의 일반성으로 진술할 것인가”라는 판단이 된다. 이 글에서는 그 균형점을 적정 일반성(right level of generality)이라고 부르기로 하자. 정리를 지나치게 특수한 조건에서만 진술하면 훗날의 적용 범위가 좁아진다. 반대로 필요 이상의 일반성을 추구하면 가정과 표기가 늘어나 핵심 아이디어가 흐려지고, 실제 사용과 유지가 어려워질 수 있다. ‘적정 일반성’은 이미 확립된 하나의 수학적 불변량이 아니라, 이 글이 연구 설계의 문제를 설명하기 위해 사용하는 분석적 표현이다.

그로텐디크의 방법론은 일반화를 올바른 방향으로 밀어 올렸을 때 얻는 힘을 잘 보여 준다. 개별 난제를 정면으로 계산하기보다, 그 문제가 자연스럽게 놓이는 더 넓은 범주와 불변량을 설계하여 복잡한 현상을 구조적으로 설명하는 방식이다. 그러나 일반화 자체가 성공을 보장하지는 않는다. 좋은 일반화는 여러 증명에서 반복되는 논리를 분리하여 하나의 정리로 만들지만, 목적 없는 일반화는 표기와 가정만 늘릴 수 있다. 다음 절에서는 하나의 적절한 일반화가 서로 다른 두 분야의 정리를 어떻게 같은 뼈대 아래 놓는지 대수학의 사례로 살펴본다.

가군, 벡터공간의 확장

벡터공간은 덧셈에 관한 아벨군과 체의 스칼라 작용으로 이루어지며, 덧셈·스칼라곱에 관한 여러 공리를 만족한다. 여기서 체를 일반적인 환으로 바꾸면 가군(module, 모듈)을 얻는다. 이 글에서는 \(1\)을 갖는 가환환 \(R\)과 그 위의 \(R\)-가군을 다루지만, 일반적으로는 비가환환 위의 왼쪽 가군과 오른쪽 가군도 정의할 수 있다. 체 위의 가군은 정확히 벡터공간이므로, 가군은 벡터공간을 포함하는 일반화다. 그러나 일반 가군은 자유가군일 필요가 없고, 따라서 벡터공간에서와 같은 기저가 존재하지 않을 수 있다. 유한차원 벡터공간의 기저 존재는 초등적으로 증명되며, 임의 차원 벡터공간의 기저 존재에는 통상 선택공리가 사용된다.[ConradModules]

이제 환 \(R\)에 적절한 제약을 주자. \(0\)이 아닌 두 원소의 곱이 \(0\)이 되지 않는 가환환을 정역(integral domain)이라고 한다. 모든 아이디얼이 어떤 한 원소로 생성되는 정역을 주 아이디얼 정역(principal ideal domain, PID)이라고 부른다. 정수환 \(\mathbb Z\)와 체 \(F\) 위의 일변수 다항식환 \(F[x]\)는 유클리드 정역이고, 따라서 PID의 대표적 예다.[ZywinaSetiabrata2018]

PID 위에서 유한 개의 생성원으로 전체가 생성되는 가군을 살펴보면 다음 구조 정리를 얻는다. “유한생성”은 가군의 원소 수가 유한하다는 뜻이 아니라, 유한한 생성 집합이 존재한다는 뜻이다.

정리: 주 아이디얼 정역 위의 유한생성 가군의 구조
주 아이디얼 정역 \(R\) 위의 유한생성 \(R\)-가군 \(M\)에 대하여, 어떤 정수 \(r,k\geq0\)와 \(0\)이 아니고 단원도 아닌 원소 \(d_1,\ldots,d_k\in R\)가 존재하여 \[ d_1\mid d_2\mid\cdots\mid d_k \] 이고 \[ M\cong R^r\oplus R/(d_1)\oplus\cdots\oplus R/(d_k) \] 가 성립한다. \(r\), \(k\), 그리고 주 아이디얼 \((d_1),\ldots,(d_k)\)는 \(M\)에 의해 유일하게 결정된다. 따라서 \(d_i\) 자체는 단원배까지 유일하다. \(r\)은 \(M\)의 자유 랭크(free rank), \(d_i\)들은 불변인자(invariant factors)라고 부른다.[ZywinaSetiabrata2018]

이 정리의 증명 줄기는 다음과 같다. \(M\)이 \(n\)개의 생성원을 가지면 그 생성원에 표준기저를 보내는 전사 \(R^n\twoheadrightarrow M\)가 있고, 핵을 \(K\)라고 할 때 제1동형정리에 따라 \(M\cong R^n/K\)이다. PID는 뇌터환이고, PID 위 자유가군의 부분가군은 자유가군이므로 \(K\)도 유한 랭크 자유가군이다. 적절한 기저를 택하면 어떤 \(s\leq n\)과 \(a_1\mid\cdots\mid a_s\)에 대하여 \[ K=Ra_1e_1\oplus\cdots\oplus Ra_se_s \] 꼴로 정리할 수 있다. 그러면 \[ R^n/K\cong R/(a_1)\oplus\cdots\oplus R/(a_s)\oplus R^{n-s} \] 가 된다. 분해의 유일성은 소멸자 하나만으로 모든 불변인자를 복원해서 얻는 것이 아니다. 프레젠테이션 행렬의 소행렬식들이 생성하는 결정 아이디얼, 또는 그와 동등한 피팅 아이디얼(Fitting ideals)이 기저변환에 불변이라는 사실을 이용해 각 불변인자를 복원한다.[ZywinaSetiabrata2018]

[관계사상의 행렬 \(A:R^m\to R^n\)에 가역적인 행 연산과 열 연산을 적용하여 \[ PAQ=\operatorname{diag}(a_1,\ldots,a_s,0,\ldots,0),\quad a_1\mid\cdots\mid a_s \] 로 만드는 것이 스미스 표준형(Smith normal form)이다. 이는 위 기저변환을 행렬로 표현한 것이며, 정수행렬에만 국한되지 않고 PID 위의 행렬에 적용된다. 특히 \(R=\mathbb Z\)나 \(F[x]\)에서는 유클리드 알고리즘을 이용해 계산할 수 있다.[Stanley2016]]

두 얼굴의 정리

이제 이 구조 정리가 서로 다른 과목에서 배우는 결과들을 어떻게 하나의 틀로 묶는지 살펴보자.

첫 번째 맥락은 군론이다. 아벨군은 정확히 \(\mathbb Z\)-가군과 같은 데이터다. 이는 유한 아벨군에만 해당하는 말이 아니라 모든 아벨군에 해당한다.[ConradModules]

[아벨군 \(G\)의 원소 \(g\)에 대해 \(n>0\)이면 \(n\cdot g=g+\cdots+g\), \(0\cdot g=0\), \(n<0\)이면 \(n\cdot g=-((-n)\cdot g)\)로 정의한다. 그러면 아벨군은 \(\mathbb Z\)-가군이 되고, 역으로 모든 \(\mathbb Z\)-가군의 덧셈군은 아벨군이다.[ConradModules]]

유한 아벨군 \(G\)에 PID 구조 정리를 적용하면 자유 랭크는 \(0\)이어야 한다. \(r>0\)이면 \(\mathbb Z^r\)라는 무한한 자유 부분이 생기기 때문이다. 각 불변인자의 양의 대표원을 택하면 유일하게 정해지는 정수 \[ 1 < d_1\mid d_2\mid\cdots\mid d_k \] 에 대하여 \[ G\cong\mathbb Z/(d_1)\oplus\cdots\oplus\mathbb Z/(d_k) \] 를 얻는다. 이것이 유한 아벨군의 기본정리의 불변인자 형태다. 여기서 유일한 것은 정규화된 불변인자 목록이지, 선택한 순환부분군이나 그 동형사상 자체가 아니다.[ZywinaSetiabrata2018]

[\(d_i>1\)일 때 \(\mathbb Z/(d_i)\)의 덧셈군은 위수 \(d_i\)인 순환군이다. \(d_i\)를 서로소인 소수 거듭제곱 인자들로 분해하고 중국인의 나머지 정리를 적용하면, 유한 아벨군을 소수 거듭제곱 위수의 순환군들로 나타내는 기본약수 분해(elementary-divisor decomposition)를 얻는다.[ZywinaSetiabrata2018]]

두 번째 맥락은 선형대수학이다. 체 \(F\) 위의 유한차원 벡터공간 \(V\)와 선형변환 \(T:V\to V\)가 주어졌다고 하자. 다항식환 \(F[x]\)는 PID다. 다음 작용을 정의하면 \(V\)는 \(F[x]\)-가군이 된다. \[ p(x)\cdot v=p(T)(v). \] 여기서 변수 \(x\)의 작용을 선형변환 \(T\)의 작용으로 해석한다. \(V\)의 \(F\)-기저는 동시에 \(F[x]\)-생성 집합이므로 이 가군은 유한생성이다.

[\(p(x)=a_0+a_1x+\cdots+a_mx^m\)이면 \[ p(T)=a_0\operatorname{id}_V+a_1T+\cdots+a_mT^m \] 이다. 이는 기저를 고르기 전에는 선형연산자이고, 기저를 택한 뒤에야 행렬로 표현된다.[Dore2017]]

이 \(F[x]\)-가군의 자유 랭크는 \(0\)이다. 한 가지 이유는 \(F[x]\)가 \(F\)-벡터공간으로 무한차원이므로, 유한차원인 \(V\) 안에 \(F[x]\) 자유가군의 비영인 직합인자가 들어갈 수 없다는 것이다. 또는 케일리–해밀턴 정리를 사용하면 같은 결론을 얻는다.

[케일리–해밀턴 정리에 따라 특성다항식 \(\chi_T(x)\)는 \(\chi_T(T)=0\)을 만족한다. 따라서 같은 \(0\)이 아닌 다항식이 \(V\)의 모든 원소를 소멸시키고, \(V\)는 꼬임 \(F[x]\)-가군(torsion module)이다. 일반적으로 꼬임가군은 각 원소 \(v\)마다 어떤 \(0\)이 아닌 스칼라가 \(v\)를 \(0\)으로 보내는 가군을 뜻한다.[Dore2017]]

PID 구조 정리를 적용하면 비상수 다항식 \(p_1,\ldots,p_k\)가 존재하여 \[ V\cong F[x]/(p_1(x))\oplus\cdots\oplus F[x]/(p_k(x)),\quad p_1\mid\cdots\mid p_k \] 가 된다. 각 \(F[x]/(p_i)\)에서 \(\bar 1,\bar x,\ldots,\bar x^{\deg p_i-1}\)을 기저로 택하면 \(x\)를 곱하는 선형변환의 행렬은 다항식 \(p_i\)의 딸림행렬(companion matrix) \(C(p_i)\)가 된다. 따라서 적절한 기저에서 \(T\)의 행렬은 \[ \operatorname{diag}(C(p_1),\ldots,C(p_k)) \] 가 되며, 이 블록 대각행렬을 \(T\)의 유리 표준형(rational canonical form), 또는 프로베니우스 표준형이라고 한다.

[\(F[x]\)의 단원은 \(0\)이 아닌 상수다. 따라서 각 불변인자 \(p_i\)를 최고차항의 계수가 \(1\)인 모닉(monic) 다항식으로 택하면 단원배의 모호성이 사라지고 \(p_i\) 자체가 유일하게 정해진다.[Dore2017]]

이제 \(F\)가 대수적으로 닫혀 있다고 하자. 더 일반적으로는 \(T\)의 특성다항식이 \(F\) 위에서 일차식들로 완전히 분해된다고만 가정해도 충분하다. 각 불변인자를 서로 다른 \(\lambda\)에 대한 \((x-\lambda)^e\)들의 곱으로 인수분해하고 중국인의 나머지 정리를 적용하면 \[ F[x]/(p_i(x))\cong \bigoplus_{\lambda}F[x]/((x-\lambda)^{e_{i,\lambda}}) \] 와 같은 기본약수 분해를 얻는다. 각 \(F[x]/((x-\lambda)^e)\)에서 적절한 기저를 택하면 \(x\)의 곱셈행렬은 주대각선에 \(\lambda\)가 있고 인접한 한 부대각선에 \(1\)이 놓이는 조르당 블록 \(J_e(\lambda)\)이 된다. \(1\)을 위쪽에 둘지 아래쪽에 둘지는 기저 순서의 관례에 달려 있다. 이 블록들을 모은 행렬이 조르당 표준형(Jordan canonical form)이며, 블록의 순서를 제외하면 고유값과 블록 크기는 유일하게 결정된다.[ZywinaSetiabrata2018]

따라서 \(R=\mathbb Z\)인 경우에는 유한생성 아벨군의 분류가, \(R=F[x]\)인 경우에는 유리 표준형이 PID 구조 정리에서 직접 나온다. 특성다항식이 \(F\)에서 분해될 때 후자의 기본약수 분해와 중국인의 나머지 정리를 더 적용하면 조르당 표준형을 얻는다. 학부 교과서에서는 유한 아벨군의 분류와 행렬의 표준형을 서로 다른 계산법으로 가르치기도 하지만, 가군의 언어는 두 계산의 공통 뼈대를 드러낸다. 이것이 적절한 일반화가 수학의 파편화를 줄이는 한 방식이다.

컴퓨터가 요구하는 설계

‘적정 일반성’을 가늠하는 판단은 전통적으로 수학자의 경험과 학계의 관행에 크게 의존했다. 21세기에는 이 판단이 형식화된 수학 라이브러리의 소프트웨어 설계 문제로도 나타난다.

Lean(린)은 종속 유형 이론에 기반한 프로그래밍 언어이자 대화형 정리 증명기다. 사용자는 정의, 정리의 명제, 증명 항 또는 전술(tactic)을 작성하고, 정교화기와 전술이 만들어 낸 증명 항의 타입을 작은 논리 커널이 검사한다. Lean의 핵심 작동 원리는 작성된 증명 항의 기계적인 타입 검사이다.[LeanLanguageReference]

[레오나르도 드 무라(Leonardo de Moura)는 마이크로소프트 리서치에 있던 2013년에 Lean 프로젝트를 시작했고, Lean 0.1은 2014년 6월 16일 공개되었다. 이후 Lean은 여러 개발자와 사용자 공동체가 함께 발전시켰으며, 현재 드 무라는 Lean FRO의 공동 설립자이자 수석 설계자다. 따라서 “마이크로소프트의 연구자가 지금까지 단독으로 진두지휘했다”라고 쓰는 것은 현재의 소속과 공동 개발 구조를 충분히 반영하지 못한다.[LeanLanguageReference]]

Lean 위에는 Mathlib이라는 공동체 주도형 수학 라이브러리가 구축되어 있다. 이 라이브러리는 수학자, 컴퓨터과학자, 프로그래머 등 많은 기여자가 함께 유지하며, 대수학·해석학·위상수학·측도론을 비롯한 폭넓은 정의와 정리를 담고 있다. Mathlib의 내용은 ‘영구히 고정된 저장물’이 아니라 공개된 버전 관리 아래 계속 확장되고 수정되며 리팩터링되는 코드다. 2020년의 Mathlib 논문은 구조의 계층, 자동화, 정의의 표현 방식과 같은 설계 결정을 라이브러리의 핵심 특징으로 설명한다.[MathlibCommunity2020]

이 현장에서 일반성은 구체적인 비용을 갖는다. 보조정리를 지나치게 좁은 구조에만 진술하면 비슷한 정리가 여러 구조에서 중복되고 재사용이 어려워질 수 있다. 반대로 무조건 가장 약한 가정과 가장 높은 추상성을 추구하면 API가 읽기 어려워지고, 유형 클래스 탐색, 강제 변환(coercion), 컴파일 시간, 오류 메시지, 유지보수 비용이 커질 수 있다. Lean은 유형 클래스 추론과 자동화로 많은 가정을 자동 공급하므로, 일반적인 정리를 호출할 때마다 사용자가 모든 하위 가정을 수작업으로 증명해야 하는 것은 아니다. 실제 쟁점은 재사용성뿐 아니라 검색 가능성, 합성 가능성, 성능, 가독성, 향후 변경의 비용을 함께 조절하는 데 있다.

일가 기초론

이제 일반성의 문제를 수학의 기초론 자체로 옮겨 보자. 블라디미르 보에보츠키(Vladimir Voevodsky)는 2000년 전후 자신의 복잡한 논증에서 오류가 뒤늦게 발견된 경험과 고차원 구조를 신뢰성 있게 다룰 형식 체계의 필요성을 계기로, 컴퓨터 검증에 적합한 새로운 기초를 모색했다. 이 연구는 2000년대에 일가 공리와 그 모형에 관한 작업으로 발전했고, 이후 일가 기초론(univalent foundations) 프로그램으로 이어졌다.[Voevodsky2014]

여기에는 현업 수학의 구조주의적 관행과 관련된 중요한 문제도 있다. 수학자는 동형인 대상을 흔히 “동일시해도 좋다”고 말하지만, 실제 계산에서는 동형사상이나 그에 따른 구조의 운반(transport)을 사용한다. 같은 차원의 두 유한차원 벡터공간은 일반적으로 동형이지만, 선택된 동형 없이 문자 그대로 같은 집합은 아니며 그 동형도 대개 정준적이지 않다. 폰 노이만 방식과 체르멜로 방식으로 만든 자연수 \(3\) 역시 서로 다른 집합 부호화이지만, 각각이 이루는 자연수 구조는 동형이다. 고전적 집합론에서 등호와 동형을 구별하는 것은 논리적 모순이 아니다. 다만 구조적으로 불변인 수학을 형식화할 때 매번 특정 부호화와 운반을 관리해야 하는 표현상의 마찰이 생긴다.

일가 공리는 이 마찰을 정교한 방식으로 다룬다. 하나의 일가적인 우주 \(U\)에서 두 유형 \(A,B:U\)에 대하여, 동일성으로부터 동치를 만드는 표준 사상 \[ (A=_U B)\longrightarrow(A\simeq B) \] 이 그 자체로 동치라고 주장한다. 따라서 \(A\simeq B\)라는 동치로부터 \(A=_U B\)의 경로를 얻고, 그 경로를 따라 성질과 구조를 운반할 수 있다.[UnivalentFoundations2013] 일가 공리는 일가 기초론이 채택하는 핵심 원리이며, 적절한 모형을 통해 그 상대적 일관성이 보장된다.

AI와 추상화

최근에는 거대 언어 모형과 강화학습을 이용한 인공지능이 자연어 수학과 형식 증명 양쪽에 진입하고 있다. 그 방식은 두 가지로 생각할 수 있다. 첫 번째는 Lean 안에서 증명 탐색을 수행하여 커널이 검사할 수 있는 증명 항을 만드는 방식이고, 두 번째는 자연어 증명을 생성한 뒤 인간 전문가가 검토하거나 나중에 별도로 형식화하는 방식이다.

[구체적인 전자의 사례로, OpenAI는 2022년 Lean에서 형식화된 올림피아드 문제를 푸는 신경 정리 증명기를 발표했다.[PoluEtAl2022] Google DeepMind의 AlphaProof는 Lean 환경에서 강화학습과 탐색을 결합했고, AlphaGeometry 2와 함께 2024년 국제수학올림피아드에서 은메달선에 해당하는 점수를 얻었다. 이 결과는 2026년 Nature 논문으로 출판되었다.[HubertEtAl2026]]

이 발전이 ‘적정 일반성’의 판단을 어떻게 바꿀지는 아직 열린 문제다. 앞으로 AI가 여러 증명에서 반복되는 패턴을 찾아 더 재사용 가능한 보조정리를 제안하거나, 인간이 택한 가정의 일부가 불필요함을 발견할 수는 있을 것이다.

지금까지 우리는 완성된 지식을 전달받는 교실을 떠나, 미지의 문제와 맞부딪히는 연구 현장에서 추상화의 한계를 어디까지 밀어야 하는지를 둘러싼 철학적·실무적 논쟁을 살펴보았다. 가워스는 이론 구축과 문제 해결이라는 서로 다른 우선순위를 대비하되, 두 활동이 배타적인 진영이 아니며 수학에 모두 필요하다고 강조했다. 아놀드는 수학 교육에서 기하학적·물리적 직관을 밀어내는 공리적 형식주의를 비판했다. 이 두 논쟁은 어느 한쪽의 승리로 끝나기보다, 문제와 목적에 맞는 일반성의 수준을 판단해야 한다는 과제를 남긴다.

대수학의 사례에서는 PID 위 유한생성 가군의 구조 정리가 \(R=\mathbb Z\)일 때 유한 아벨군의 분류를, \(R=F[x]\)일 때 선형변환의 유리 표준형을 준다는 사실을 확인했다. 특성다항식이 바탕체에서 분해될 때 기본약수 분해를 더하면 조르당 표준형도 얻는다. 이 사례는 서로 다른 계산을 하나의 구조 아래 묶는 좋은 일반화의 힘을 보여 준다. 한편 Mathlib 같은 형식 수학 라이브러리는 일반성과 재사용성을 가독성·성능·유지보수성과 함께 설계하도록 요구한다. 일가 기초론은 더 근본적인 수준에서 동치에 따라 불변인 수학을 기초 체계에 반영하려 한다. AI 정리 증명은 이 모든 판단의 일부를 자동화할 가능성을 열었지만, 최적의 추상화를 자율적으로 설계하는 문제는 여전히 연구 과제다.

지금까지 10편에 이르는 연재는 수학적 추상화가 형성되고 사용되는 여러 장면을 따라왔다.

  • 고대 메소포타미아에서 셈돌·점토표·수 표상 사이의 관계가 변하며 구체적 사물과 수량을 표현하는 방식이 분화된 장면
  • 르네상스와 근대 초기에 기호가 미지수와 연산 관계를 간결하게 표현하며 대수학의 일반 법칙을 드러낸 장면
  • 19세기 말 공리 체계가 기하학의 암묵적 전제를 드러내고, 점과 직선의 구체적 성질보다 관계를 통해 대상을 규정한 장면
  • 현대 범주론이 대상뿐 아니라 대상 사이의 사상과 그 합성을 중심에 놓아 서로 다른 구조 사이의 공통 패턴을 표현한 장면

그리고 이 모든 개념이 배우고 전수되는 강의실, 새 정리와 정의를 설계하는 연구 현장, 이를 형식 코드로 조직하는 디지털 라이브러리 역시 추상화의 역사가 계속되는 장소다.

이제 이 긴 지적 여정을 한자리에 모아 종합적으로 갈무리할 때가 되었다. 수학자들이 자주 함께 사용하는 ‘추상화’와 ‘일반화’, ‘이상화’와 ‘형식화’라는 네 가지 논리적 조작은 어떻게 구별되는가? 이 연재에서 살펴본 여러 추상화 방식은 수학의 거대한 그물망 속에서 어떻게 이어지는가? 그리고 이 추상적 대상들은 인간과 무관하게 존재하는 플라톤적 실재인가, 아니면 인간이 만든 기호적 구성물인가? 이어지는 11부에서 이러한 철학적 주제를 탐구해 보자.

참고문헌

저작권

이슬비, 2026. designeralice＠daum.net.

수학적 추상화

  1. 수학적 추상화의 기본 개념
  2. 초기 수학에서의 암묵적 추상화
  3. 대수적 기호와 연산 법칙
  4. 공리적 방법에 의한 추상화
  5. 수학적 구조와 범주론
  6. 벡터공간과 선형 구조
  7. 거리공간과 위상공간
  8. 측도공간과 확률공간
  9. 수학적 추상화의 인지와 학습
  10. 현대 수학 연구에서의 추상화
  11. 수학적 추상화의 방법과 철학