Dilatations of categories, via their lean formalization

수학의 광활한 풍경을 고립된 섬들의 집합이 아니라, 거대하고 서로 연결된 하나의 도시라고 상상해 보십시오. 이 도시에서 **범주론(Category Theory)**은 숙련된 지도 제작자입니다. 범주론은 건물의 세부 사항(그 건물이 벽돌로 만들어졌는지 나무로 만들어졌는지 등)에는 관심을 두지 않습니다. 대신, 건물들을 연결하는 도로와 그 사이를 이동하기 위한 규칙에 관심을 가집니다. 이 "건물들"을 **대상(objects)**이라 부르고, "도로"를 **사상(morphisms, 또는 화살표)**이라고 부릅니다.

때때로 수학자들은 여행을 더 쉽게 만들기 위해 도시의 규칙을 바꾸고 싶어 합니다. 전형적인 기법 중 하나는 **국소화(localization)**입니다. 국소화는 현재 막다른 길인 도로를 양방향 도로로 바꾸거나, 통행료 징수소를 완전히 제거하여 교통이 뒤로도 흐를 수 있게 하거나 자유롭게 통과할 수 있도록 만드는 것과 같습니다. 이는 대수학에서 기하학에 이르기까지 도처에서 사용되는 강력한 도구입니다.

하지만 도로를 완전히 없애고 싶지는 않을 수도 있습니다. 대신, 나머지 교통 규칙은 그대로 유지하면서 특정 특정한 배달물들만 통과할 수 있도록 만들고 싶다면 어떨까요? 여기서 **딜라타시옹(dilatation, 확장)**이 등장합니다. 이것은 국소화의 "정교한" 버전이라고 생각하면 됩니다. 전체 게이트를 여는 대신, 특정 열쇠(체, sieve)를 동반했을 때만 특정 문을 통해 특정 패키지(사상)가 통과할 수 있는 특별하고 좁은 우회 차선을 만드는 것입니다. 이는 일반적인 국소화보다 훨씬 더 정밀하고 외과적인 작업입니다.

왜 이런 것에 관심을 가질까요? 왜냐하면 이러한 수학적 구조는 우리가 모양, 공간, 심지어 컴퓨터 프로그램의 논리를 이해하는 근간이 되는 코드이기 때문입니다. 만약 우리가 이 규칙들이 완벽하게 작동한다는 것을 증명할 수 있다면, 우리는 더 신뢰할 수 있는 소프트웨어를 구축하고 물리학 및 공학의 복잡한 문제들을 해결할 수 있습니다. 그러나 인간의 수학은 아주 작고 눈에 보이지 않는 오류, 즉 누락된 "if" 문이나 약간 모호한 가정에 취약합니다. 이것이 바로 이 논문이 특별한 이유입니다. 이 논문은 단순히 수학을 적어 내려가는 것이 아니라, 논리가 깨지지 않도록 모든 단계와 모든 줄을 컴퓨터가 한 줄 한 줄 검증하도록 강제합니다.

---

논문: 수학적 수술을 위한 디지털 청사진

"Dilatations of Categories, Via Their Lean Formalization"이라는 제목의 이 논문은, 수학자 아르노 마이외(Arnaud Mayeux)가 이 "정교한 도로 규칙"(딜라타시옹)에 관한 출판된 수학 이론을 컴퓨터가 이해하고 검증할 수 있는 언어로 완전히 번역한 거대한 프로젝트에 대한 보고서입니다. 사용된 컴퓨터 도구는 Lean 4이며, 이는 Mathlib이라 불리는 검증된 수학의 거대한 라이브러리 안에 존재합니다.

원래의 수학 논문을 손으로 그린 건축 설계도라고 생각해 보십시오. 그것들은 올바르게 보이고 다른 건축가들도 고개를 끄덕였겠지만, 종이 위에 작은 얼룩이 있거나 인간의 눈에는 "당연해" 보여서 실제로 중요한 세부 사항을 건너뛴 단계가 있을 수 있습니다. 마이외의 작업은 그 설계도를 가져와서 실수를 할 수 없는 디지털 3D 모델링 소프트웨어로 재구축하는 것이었습니다. 만약 수학이 완벽하게 맞물리지 않으면, 소프트웨어는 코드 컴파일을 거부합니다.

주요 발견: 새로운 구축 방식
이 논문의 가장 큰 발견은 단순히 수학이 옳다는 것이 아니라, 그 수학이 어떻게 구축되었는가 하는 점입니다. 원래의 이론에서 "딜라타시옹"은 특정 방식으로 접착된 "분수"(예: $n/d$)들의 집합으로 설명되었습니다. 이것을 손으로 하는 것은 마치 벽이 수직인지 매번 확인하며 벽돌을 하나씩 쌓아 집을 짓는 것처럼 지저분한 일입니다.

마이외의 형식화는 다른, 더 스마트한 경로를 택했습니다. 벽돌을 쌓는 대신, 그들은 먼저 "골격"(연결되지 않은 가공의 범주)을 만든 다음, 컴퓨터가 생성한 "몫(quotient)"을 사용하여 규칙에 따라 조각들을 딱 맞게 끼워 넣었습니다. 이 접근 방식은 물리 법칙을 알고 있는 3D 프린터를 사용하는 것과 같습니다. 벽이 수직인지 수동으로 확인할 필요가 없습니다. 규칙이 기계 안에 내장되어 있기 때문입니다. 이 방법을 통해 팀은 딜라타시옹의 "보편적 성질"(이 특정 우회로를 만드는 유일한 방법이라는 규칙)을 절대적인 확신을 가지고 증명할 수 있었습니다.

반전: 원본 논문에 결함이 있었다면?
여기서 이야기는 흥부터 흥미로워집니다. 컴퓨터는 매우 엄격하기 때문에, 원본 논문에서 미세하게 어긋난 두 곳을 찾아냈습니다.

1. "정규성"의 함정: 한 섹션에서, 원본 논문은 특정 수학적 연산(두 딜라타시옹을 결합하는 것)이 마치 실패하지 않는 마술처럼 항상 완벽하게 작동한다고 주장했습니다. 그러나 컴퓨터는 이렇게 말했습니다. "잠깐만요. 이 작업은 특정 추가 조건이 있어야만 작동합니다." 형식화를 통해, 이 추가 조건이 없다면 그 마술은 실패한다는 것이 밝혀졌습니다. 이 결과가 원본 수학이 쓸모없다는 것을 의미하는 것은 아니지만, 원본의 주장이 너무 광범-적이었다는 것을 입증했습니다. 이는 마치 "모든 새는 날 수 있다"라고 말했다가 펭귄의 존재를 깨닫게 된 것과 같습니다. 논문은 그 규칙이 참이 되도록 하기 위해 "펭귄 예외"를 추가해야 했습니다.
2. 환(Ring)과 범주의 혼동: 논문은 또한 이 범주 규칙을 "가환 환(commutative rings, 일종의 대수)"의 규칙과 비교했습니다. 원본 논문은 특정 규칙이 두 경우 모두에 적용된다고 제안했습니다. 컴퓨터는 단 두 개의 대상과 몇 개의 화살표로 이루어진 아주 작은 수학적 퍼즐(반례)을 찾아냈는데, 여기서는 규칙이 환에서는 작동하지만 범주에서는 완전히 깨졌습니다. 이는 자동차(환)용으로 설계된 다리 디자인이 자전거(범주)를 타고 건너려 하면 무너질 수 있다는 발견과 같습니다. 논문은 이 두 이론이 이 점에서 동일하다는 아이디어를 명시적으로 배제합니다.

"코딜라타시옹(Codilatation)"이라는 지름길
논문은 또한 "코딜라타시옹"이라는 영리한 기법을 소개합니다. 반대 방향(화살표가 뒤로 향하는 방향)을 위한 새로운 규칙 책을 쓰는 대신, 형식화는 단순히 "지도를 뒤집자"라고 말했습니다. 컴퓨터의 즉각적인 좌우 반전 능력을 활용하여, 팀은 새로운 증명을 단 하나도 작성하지 않고도 역방향에 대한 규칙을 증명했습니다. 이는 만약 당신이 앞으로 운전하는 법을 안다면, 핸들을 반대로 돌리기만 하면 이미 뒤로 운전하는 법을 알고 있는 것과 같습니다.

결론
이 논문은 "형식화된 수학"의 승리입니다. 이는 딜라타시옹 이론이 견고하다는 것을 증명할 뿐만 아니라, 인간의 눈이 놓친 원본 이론의 미세한 균열을 찾아내고 수정하는 품질 관리 검사관의 역할도 수행합니다. 이는 복잡한 수학을 컴퓨터가 이해하는 언어로 번역할 때, 단순히 검증을 얻는 것이 아니라 수학 자체에 대한 더 명확하고 정밀한 이해를 얻게 된다는 것을 보여줍니다. 논문은 딜라타시옹 이론이 탄탄하지만 이전 생각보다 더 주의 깊은 조건들을 필요로 한다고 결론지으며, 향후 이 "정교한 도로 규칙"을 사용하고자 하는 모든 이들을 위해 컴퓨터로 검증된 완전한 사전을 제공합니다.