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

数学の宇宙を、巨大で無限の遊び場だと想像してみてください。長い間、ここでの最も人気のあるゲームは**ホモトピー型論（HoTT）**でした。このゲームでは、すべてが完璧に柔軟な「形」で構成されています。もし点Aから点Bへのパス（経路）があるなら、常にそれを逆方向に歩むことができます。それは、あらゆる引き伸ばしが元の状態にパチンと戻せる、弾力性のあるゴムバンドのような世界です。これは「空間」（すべてのものが可逆的である数学的対象）を研究するには素晴らしいのですが、方向性のある一方通行の道が存在するカテゴリーという、より複雑で現実的な世界には、少し完璧すぎます。

そこに、Nikolai Kudasov、Violetta Sim、Benedikt Ahrensによって構築された新しい証明助手であるRzkが登場しました。Rzkを、方向性のある形（directed shapes）を構築するために設計された特化型のコンストラクション・キットだと考えてください。この新しい遊び場では、AからBへのパスがあっても、それを逆方向に歩むことはできません。それは、接続が永続的であるLEGOブロックで組み立てるようなものです。パーツをはめ込むことはできますが、モデルを壊さずにそのままでは外すことはできません。これにより、数学者は、矢印（射）に方向性があり、必ずしも逆転しない構造である$\infty$-カテゴリーを推論できるようになります。

大きなアイデア：新しい構築方法

この論文は、Rzkを、Emily RiehlとMichael Shulmanによって提案された**Simplicial Type Theory (RSTT)**という特定の理論を実装するツールとして紹介しています。

Rzkが使う巧妙なトリックは以下の通りです：
元の理論（RSTT）には、**拡張型（extension type）**と呼ばれる特別な「魔法の箱」がありました。この箱を使うと、図形の「エッジ（辺）」（例えば三角形）の上では特定の挙ニックに振る舞い、その内部ではどのように振る舞ってもよい関数を定義できました。これは強力でしたが、一種のブラックボックスのようなもので、そのルールが細則の中に隠されていることがありました。

Rzkはこの魔法の箱を分解して開けます。

1. 形（Shape）： 「形」（三角形や区間）の部分と、「境界（boundary）」（エッジに関するルール）の部分を分離します。
2. ルール： 強制変換（coercion）のないサブタイピングという、新しい明示的なルールを導入します。あなたが小さな箱に収まるおもちゃの車を持っていると想像してください。旧システムでは、システムはチェックすることなく、その車がより大きな箱に収まると「想定」していました。Rzkでは、システムは車が収まるかどうかを明示的にチェックしますが、その車を大きな箱に合わせるために余計な梱包材で包むこと（強制変換）を強要しません。単に、「はい、この車はまたおもちゃでもあるので、おもちゃの箱に属しています」と言うのです。これにより、論理はよりクリーンになり、コンピュータによる検証が容易になります。

Rzkができること（できないこと）

著者たちは、この新しいシステムの「標準ライブラリ」としてsHoTTを構築しました。これはすでに膨大であり、25,000行以上のコードと、1,500近いトップレベルの宣言を含んでいます。このライブラリは、$\infty$-カテゴリー的ヨネダ補題（カテゴリー論における基本的な定理）や、様々な種類の「ファイブレーション」（カテゴリーを積み重ねる方法）といった複雑な概念の形式化に成功しています。

しかし、論文では自身が何を証明したかについて非常に慎重に述べています：

• 忠実である（Faithful）： 著者らは、元の理論（RSTT）で証明できることは、Rzkでも証明できることを証明しました。これは完璧な翻訳です。
• 保守的である（Conservative）（ただし、注釈あり）： Rzkは、古い理論について新しい真理を捏造しないことを証明しました。Rzkが古い図形について何かを証明できるなら、古い理論もそれを証明できたはずです。ただし、この証明は特定の「自然な断片（natural fragment）」の導出に対してのみ機能します。著者らは、すべての奇妙なケースについて完全に証明したわけではないことを認めています。彼らは、これが全体系において一般的に成立すると推測していますが、まだ**予想（conjecture）**の段階です。
• 実用的である（Practical）： このツールは今すぐ使えます。ウェブブラウザで動作し、VS Code拡張機能があり、サマースクールや修士論文でも使用されています。

「シェイプ・ソルバー（形の解決器）」

この数学の最も難しい部分の一つは、ある形が別の形の中に収まっているかどうか（例：この三角形は正方形の中にあるか？）をチェックすることです。Rzkは、これを解決するために自動化された「トープ・ソルバー（tope solver）」を使用しています。

• 仕組み： それは、パズルを解こうとする探偵のようなものです。ルール（トープ）を調べ、それらが適合するかどうかを試みます。
• 性能は？： sHoTTライブラリを用いたテストでは、ソルバーは25,000件以上の質問を処理しました。ほとんどは即座に（1ステップで）解決されました。非常に困難なものもいくつかあり、数千ステップを要しましたが、ソルバーはそれらを処理できました。
• 限界： このソルバーは不完全です。これはプロトタイプです。目の前の問題にはうまく機能しますが、すべての可能な経路を試そうとしないため、トリッキーな解決策を見逃す可能性があることを著者らは認めています。将来的に「完璧な」ソルバーを構築する予定ですが、現時点では、現在のものは「実用上は十分」です。

Rzkが拒絶するもの

この論文は、図形の包含関係（例：この三角形は正方形の中にある）をすべて手動で証明する必要があるという考えに対し、明確に反対しています。古いシステムでは、「この三角形は正方形の中にある」と言うためだけに長い証明を書かなければならないことがありました。Rzkはこの手作業を拒絶し、それを自動化します。

また、強制変換（coercions）（物事を適合させるために余計な梱包層を追加すること）という考えも拒絶します。著者らは、数学を複雑にする目に見えない変換ステップをコンピュータに挿入させることなく、サブタイプを理解できるシステムを持つことができる、ということを示しています。

結論

Rzkは、方向性のある無限カテゴリーの抽象的な理論を、コンピュータによる証明という現実の世界へと持ち込む、実際に動作する利用可能なツールです。それは複雑な数学的「魔法の箱」を、より単純で透明な部分へと分解し、新しい能力を加えつつも、古いルールを壊さないことを証明しています。

著者たちは、Rzkが理論を忠実に実装していること、そして彼らのライブラリが機能していることに自信を持っています。彼らは、このツールが今日の教育や研究において有用であると確信しています。しかし、すべてのエッジケースに対する完全な理論的保証（「完全な保守性」の予想）については確信が持てず、シェイプ・ソルバーが改善の余地のあるプロトタイプであることを認めています。また、システムがすべての入力に対して停止すること（正規化）を保証するという問題は、将来の課題として残っています。

要約すれば、Rzkは、新鮮な設計によってコンピュータの仕事を容易にしつつ、元の理論の魔法を失うことなく、新しい種類の数学のための、動作し、検証され、成長し続けているエンジンなのです。