가압성(Compressibility)이 전부다

Michael Mulligan의 강연 영상에서 핵심 관점은 "인간 수학(Human Math)"과 "형식 수학(Formal Math)"의 근본적인 차이가 매우 높은 "가압성(Compressibility)"을 갖추고 있다는 점입니다. 강연자는 군론(Group Theory)의 단항군(Monoids)을 장난감 모델로 도입하고, Lean 언어의 수학 라이브러리(Mathlib)를 결합한 실증 연구를 통해, 인간 수학이 계층적으로 중첩된 정의와 정리(Theorem)를 통해 고도로 압축되어 있음을 논증합니다.

다음은 영상 내용의 매우 상세한 분석입니다:

1. 핵심 개념 도입: 인간 수학 vs 형식 수학

형식 수학 (Formal Math): 논리적으로 합법적인 모든 추론과 증명을 포함하는 거대한 공간입니다. 이 공간은 극도로 방대하며, 심지어 지수적으로 폭발하며 성장한다고 할 수 있습니다.
인간 수학 (Human Math): 인간이 실제로 발견하고 이해하며 논문이나 라이브러리(예: arXiv)에 기록한 수학은 형식 수학이라는 이 광활한 대양 속의 매우 작은 부분집합일 뿐입니다 [00:00:21].
핵심 문제: 우리는 이 대양 속에서 어떻게 "인간 수학"이라는 작은 구석을 정확하게 찾아내고 식별할 수 있을까요? 강연자는 **고차원적인 중첩 정의(Hierarchical Nesting)와 이로 인해 발생하는 "가압성(Compressibility)"**이 인간 수학의 가장 현저한 특징이라고 제안합니다 [00:00:52].

2. 이론 모델: "단항군"에 기반한 논리 시뮬레이션

이러한 "압축"이 어떻게 작동하는지 정량화하기 위해, 연구팀은 단항군(Monoids)을 이용하여 수학적 추론을 시뮬레이션하는 장난감 모델(추론 트리를 문자 흐름/문자열로 펼침)을 구축했습니다 [00:02:16]. 그들은 두 가지 극단적인 단항군을 비교했습니다:

아벨 단항군 (Abelian Monoid):
- 자연수의 덧셈과 유사하며, 문자의 순서는 중요하지 않고 문자가 나타나는 횟수(다중 집합)만 고려합니다.
- 공간 성장이 매우 느리며, **다항식 성장 공간 (Polynomial-growth space)**에 속합니다 [00:02:59].
자유 단항군 (Free Monoid):
- 교환법칙이 성립하지 않으며, 문자의 배열 순서가 매우 중요합니다 (마치 실제 논리적 추론처럼 단계의 순서가 틀려서는 안 됩니다).
- 공간이 극도로 방대하며, **지수 성장 공간 (Exponential-growth space)**을 형성합니다 [00:03:21].

"매크로(Macros)"의 도입과 레버리지 효과

모델에서 그들은 "새로운 기호" 또는 "정의"(즉, 매크로 집합 $M$)를 도입했는데, 이는 인간 수학에서 끊임없이 새로운 개념을 발명하는 것(예: 덧셈을 정의한 후 곱셈을 정의하고, 다시 거듭제곱을 정의하는 것)과 유사합니다.

아벨 단항군에서: 희소한 매크로 집합(적은 수의 정의)을 도입하는 것만으로도 지수적인 표현력 (Expressivity)(즉, "위치 표기법 Place notation")을 가져올 수 있습니다. 만약 조금 더 큰 매크로 집합을 도입한다면, "워링의 정리 (Waring's theorem)"를 이용하여 무한한 표현력을 얻을 수도 있습니다 [00:04:51].
자유 단항군에서: 매우 밀집된 매크로 집합을 도입하더라도 추가적인 표현 효율을 얻기가 거의 불가능합니다. 더 많은 것을 표현하려면 거의 모든 요소에 대해 개별적으로 이름을 붙여야 하며, 이는 "새로운 기호의 정의"를 무의미하게 만듭니다 [00:05:35].

직관적으로 수학적 추론은 "자유 단항군"(순서가 중요함)과 더 유사해야 하지만, 실험 결과는 놀랍도록 반직관적인 결론을 보여주었습니다.

3. 실증 연구: Lean 수학 라이브러리 (Mathlib)의 데이터 성능

이론을 검증하기 위해 연구팀은 약 50만 개의 수학적 요소를 포함하는 Lean 언어의 Mathlib를 "인간 수학"의 대리 데이터셋으로 사용하여 측정했습니다 [00:06:01]. 그들은 라이브러리의 각 수학적 요소(정리/정의)에 대해 세 가지 핵심 지표를 측정했습니다 [00:06:47]:

포장 길이 (Wrap Length): 해당 요소가 Lean 코드에서 정의될 때의 원시 토큰(Token) 수 (즉, 인간이 보는 정리의 약어 길이).
해제 길이 (Unwrap Length): 해당 정리에서 사용된 모든 정의와 정리를 가장 기초적인 공리/원시 개념(Primitives)까지 재귀적으로 분해하여 복원했을 때 최종적으로 필요한 총 토큰 수.
깊이 (Depth): 해당 정리로부터 시작하여 의존성 체인을 통해 기초 공리까지 거슬러 올라가는 데 필요한 가장 긴 경로.

놀라운 측정 결과:

해제 길이 (Unwrap Length) vs 깊이: 깊이가 증가함에 따라, 정리를 완전히 해제했을 때의 길이는 뚜렷한 지수적 폭발 성장을 보입니다 [00:07:29].
포장 길이 (Wrap Length) vs 깊이: 해제 후의 길이는 천문학적인 숫자가 되지만, 인간의 코드에 나타나는 포장 길이는 기본적으로 **선형적 성장 (매우 완만함)**을 유지합니다 [00:08:04].

이는 인간의 수학이 끊임없이 심연을 향해 나아갈 때, 층층이 쌓인 '새로운 정의 (New definitions)'라는 마트료시카(Matryoshka) 방식을 통해, 논리적으로는 지수 함수적으로 폭발하는 복잡한 구조를 인간의 두뇌와 코드가 처리할 수 있는 선형적 복잡도 (Linear complexity)로 압축하는 데 성공했음을 의미합니다.

4. 모델 비교 및 최종 결론

Mathlib의 실제 데이터를 앞서 언급한 반군 (Semigroup) 토이 모델과 매칭했을 때, 결과는 다음과 같습니다 [00:08:13]:

대부분의 자유 반군 (Free semigroup, 비가환 및 순서 중시) 모델은 모두 실패로 판명되었으며, 이러한 높은 압축률을 설명하지 못했습니다.
기이하게도, 실제 데이터와 잘 일치하는 유일한 모델은 바로 **단순해 보이는 아벨 반군 (Abelian semigroup, 자릿수 표기법)**이었습니다 [00:08:41].

최종 추론: 인간의 수학은 형식 수학 (Formal mathematics)이라는 끝없는 바다 속에서, 마치 "다항식 성장 (Polynomial growth) 공간 내에서 희소한 거대 집합 (Sparse macro-set)을 가진 특례"처럼 행동합니다. 인간 수학의 본질은 압축 가능한 논리 구조를 찾는 것입니다 [00:08:51].

5. 미래 전망: AI 자동 추론 (Automated Reasoning) 가이드

'압축성 (Compressibility)'이 인간 수학의 등대라면, 이를 사용하여 AI 증명 에이전트 (Agents)를 가이드할 수 있을까요? 발표자는 다음과 같은 구체적인 구상을 제안했습니다 [00:09:02]:

압축 지표 구축: '환원 압축률 (Reductive compression)'과 같은 지표를 설계하여, 압축 복잡도 측면에서 특정 정의가 기여하는 바를 평가합니다. 또는 간결한 진술이 매우 깊은 증명에 대응하는지를 평가합니다.
PageRank 알고리즘 결합: Mathlib의 의존성 그래프 (Dependency graph) 상에서 표준 PageRank (페이지랭크) 알고리즘을 실행하되, 앞서 언급한 '압축 지표'를 가중치 편향 (Weight bias)으로 주입합니다 [00:09:42].
응용 시나리오: 이 가중치가 적용된 PageRank를 통해 고정점 점수 (Fixed-point score)를 계산함으로써, 향후 AI가 정리 증명 (Theorem proving)을 수행할 때 '전제 선택 (Premise Selection, 즉 현재 정리를 증명할 때 어떤 기지의 정리와 개념이 가장 중요하고 관련이 있는지 AI가 알 수 있도록 하는 것)'을 수행하는 데 큰 도움을 줄 수 있을 것입니다 [00:10:08].