Rzk: a Proof Assistant for Synthetic $\infty$-Categories

수학의 우주를 거대한, 무한한 놀이터라고 상상해 보십시오. 오랫동안 이곳에서 가장 인기 있는 게임은 **호모토피 유형론(Homotopy Type Theory, HoTT)**이었습니다. 이 게임에서 모든 것은 완벽하게 유연한 "형태(shapes)"로 이루어져 있습니다. 만약 점 A에서 점 B로 가는 경로가 있다면, 당신은 언제나 그 길을 되돌아올 수 있습니다. 이것은 마치 모든 늘어남이 원래 상태로 다시 돌아올 수 있는 탄성 밴드의 세계와 같습니다. 이는 "공간"(모든 것이 가역적인 수학적 대상)을 연구하는 데는 훌륭하지만, 어떤 경로는 일방통행인 카테고리라는 복잡하고 실제적인 세상에는 조금 너무 완벽합니다.

여기에, 니콜라이 쿠다소프(Nikolai Kudasov), 비올레타 심(Violetta Sim), 베네딕트 아렌스(Benedikt Ahrens)가 만든 새로운 증명 보조기인 Rzk가 등장했습니다. Rzk를 **방향성이 있는 형태(directed shapes)**를 만들기 위해 설계된 특화된 조립 키트라고 생각하십시오. 이 새로운 놀이터에서는 A에서 B로 가는 경로는 있지만, 그 길을 되돌아갈 수는 없는 경로가 존재할 수 있습니다. 이것은 어떤 연결 부위는 영구적이어서, 조각을 끼워 넣을 수는 있지만 모델을 망가뜨리지 않고는 다시 뺄 수 없는 레고 블록으로 만드는 것과 같습니다. 이를 통해 수학자들은 화살표(모orphism)에 방향이 있고 항상 역방향이 존재하지 않는 복잡한 구조인 **$\infty$-카테고리($\infty$-categories)**를 추론할 수 있습니다.

핵심 아이디어: 구축하는 새로운 방법

이 논문은 Rzk를 에밀리 리(Emily Riehi)와 마이클 슐먼(Michael Shulman)이 제안한 **심플리셜 유형론(Simplicial Type Theory, RSTT)**이라는 특정 이론을 구현하는 도구로 소개합니다.

Rzk가 사용하는 영리한 트릭은 다음과 같습니다:
원래의 이론(RSTT)에는 **확장 유형(extension type)**이라는 특별한 "마법 상자"가 있었습니다. 이 상자는 함수가 형태(예: 삼각형)의 *가장자리(edges)*에서는 특정 방식으로 동작하도록 정의하면서도, 그 중심부에서는 무엇이든 원하는 대로 할 수 있게 해주었습니다. 이는 강력했지만 블랙박스와 같아서, 그 규칙이 어떻게 작동하는지가 때때로 세부 사항 속에 숨겨져 있었습니다.

Rzk는 이 마법 상자를 가져와 그것을 쪼개어 열었습니다.

1. 형태(The Shape): 형태 부분(삼각형이나 구간)과 경계(boundary) 부분(가장자리에 대한 규칙)을 분리합니다.
2. 규칙(The Rules): **강제 변환이 없는 하위 유형(coercion-free subtyping)**이라는 새로운 명시적 규칙을 도입합니다. 당신이 작은 상자에 들어가는 장난감 자동차를 가지고 있다고 상想像해 보십시오. 이전 시스템에서는 시스템이 확인 절차 없이 자동차가 더 큰 상자에 들어갈 것이라고 그냥 가정했습니다. Rzk에서, 시스템은 자동차가 적합한지 명시적으로 확인하지만, 그 자동차를 큰 상자에 맞추기 위해 추가적인 포장(강제 변환, coercion)을 입히도록 강요하지는 않습니다. 그저 "네, 이 자동차는 또한 장난감이므로 장난감 상자에 속합니다"라고 말할 뿐입니다. 이는 논리를 더 깔끔하고 컴퓨터가 확인하기 쉽게 만듭니다.

Rzk가 할 수 있는 것 (그리고 할 수 없는 것)

저자들은 이 새로운 시스템을 위한 sHoTT라는 "표준 라이브러리"를 구축했습니다. 이 라이브러리는 이미 25,000행 이상의 코드와 거의 1,500개의 최상위 선언을 포함할 정도로 방대합니다. 이 라이브러리는 $\infty$-카테고리적 요네다 보조정리($\infty$-categorical Yoneda lemma)(카테고리 이론의 근본적인 정리)와 다양한 유형의 "파이버레이션(fibrations)"(카테고리를 쌓아 올리는 방식)과 같은 복잡한 개념들을 성공적으로 형식화했습니다.

하지만 논문은 자신이 무엇을 증명했는지에 대해 매우 신중하게 기술하고 있습니다:

• 충실함(Faithful): 저자들은 원래의 이론(RSTT)에서 증명할 수 있는 것은 무엇이든 Rzk에서도 증명할 수 있다는 것을 증명했습니다. 이는 완벽한 번역입니다.
• 보수성(Conservative, 단 단서가 있음): 저자들은 Rzk가 기존 이론에 대해 새로운 진리를 만들어내지 않는다는 것을 증명했습니다. 만약 Rzk가 기존의 형태에 대해 무언가를 증명한다면, 기존 이론도 그것을 증명할 수 있었습니다. 하지만, 이 증명은 특정 "자연스러운 파편(natural fragment)"의 유도에 대해서만 작동합니다. 저자들은 자신들이 아직 모든 가능한 기이한 경우에 대해 이 것을 완전히 증명하지 못했음을 인정합니다. 그들은 이것이 전체 시스템에 대해서도 일반적으로 성립할 것이라고 추측하지만, 이는 여전히 추측(conjecture) 단계입니다.
• 실용성(Practical): 이 도구는 지금 바로 작동합니다. 웹 브라우저에서 실행되며, VS Code 확장 프로그램을 갖추고 있고, 여름 학교와 석사 학위 논문에서도 사용되었습니다.

"형태 해결사(Shape Solver)"

이 수학의 가장 어려운 부분 중 하나는 하나의 형태가 다른 형태 안에 포함되는지(예: 이 삼각형이 이 사각형 안에 있는가?)를 확인하는 것입니다. Rzk는 이를 위해 자동화된 "토포 해결사(tope solver)"를 사용합니다.

• 작동 방식: 이것은 마치 퍼즐을 풀려는 탐정과 같습니다. 규칙(topes)을 살펴보고 그것들이 서로 맞는지 확인합니다.
• 얼마나 좋은가? sHoTT 라이브러리에 대한 테스트에서, 해결사는 25,000개 이상의 질문을 처리했습니다. 대부분은 즉시(단 한 단계 만에) 해결되었습니다. 몇몇은 매우 어려워 수천 단계를 거쳐야 했지만, 해결사는 이를 수행해 냈습니다.
• 한계: 이 해결사는 **불완전(incomplete)**합니다. 이것은 프로토타입입니다. 현재 보고 있는 문제들에 대해서는 잘 작동하지만, 저자들은 이 해결사가 모든 가능한 경로를 시도하지 않기 때문에 까다로운 해결책을 놓칠 수도 있음을 인정합니다. 그들은 미래에 "완벽한" 해결사를 만들 계획이지만, 현재의 해결사는 "실제적인 측면에서 충분"합니다.

Rzk가 거부하는 것들

논문은 모든 미세한 형태의 포함 관계를 수동으로 증명해야 한다는 생각에 명시적으로 반대합니다. 오래된 시스템에서는 "이 삼각형이 이 사각형 안에 있다"라고 말하기 위해서도 긴 증명을 직접 작성해야 했을 수도 있습니다. Rzk는 이러한 수동 노동을 거부하며, 이를 자동화합니다.

또한 이들은 강제 변환(coercions)(물건을 맞추기 위해 추가적인 포장 층을 더하는 것)의 개념을 거부합니다. 저자들은 하위 유형을 이해하면서도, 수학을 복잡하게 만드는 보이지 않는 변환 단계를 컴퓨터가 삽입하도록 강요하지 않는 시스템을 가질 수 있음을 보여줍니다.

결론

Rzk는 방향성 있는 무한 카테고리라는 추상적인 이론을 실제 컴퓨터가 검증 가능한 증명의 세계로 가져오는, 실제로 작동하고 사용 가능한 도구입니다. 이 도구는 복잡한 수학적 "마법 상자"를 더 단순하고 투명한 부분들로 나누며, 원래의 규칙을 깨뜨리지 않으면서도 새로운 능력을 추가한다는 것을 증명합니다.

저자들은 Rzk가 이론을 충실히 구현하고 있으며, 자신들의 라이브러리가 작동한다는 점에 확신하고 있습니다. 그들은 이 도구가 오늘날의 교육과 연구에 유용하다는 점을 확신합니다. 그러나 모든 가능한 예외적인 경우에 대한 완전한 이론적 보증(전체 보수성 추측)에 대해서는 덜 확신하며, 자신들의 형태 해결사가 개선될 수 있는 프로토타입임을 인정합니다. 또한 시스템이 모든 가능한 입력에 대해 종료됨을 보장하는 문제(정규화, normalization)를 아직 해결하지 못했으며, 이는 미래의 과제로 남아 있습니다.

요약하자면, Rzk는 원래 이론의 마법을 잃지 않으면서도 컴퓨터의 작업을 더 쉽게 만드는 새로운 설계를 바탕으로 구축된, 새롭고 검증되었으며 성장하는 새로운 종류의 수학 엔진입니다.