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プリンターを使うようなものです。壁が真っ直ぐであることを手動でチェックする必要はありません。なぜなら、ルールが機械の中に組み込まれているため、プリンターがそれを保証するからです。この手法により、チームは「普遍性（universal property）」（これは特定のバイパスを構築する唯一の方法であるというルール）を絶対的な確信を持って証明することができました。

プロットの急展開：元の論文にグリッチがあったとき
ここから物語は面白くなります。コンピュータは非常に厳格であるため、元の出版された論文の中に、わずかに誤っていた箇所を2つ発見しました。

1. 「正規」の罠： あるセクションにおいて、元の論文は、ある種の数学的操作（二つの拡張を組み合わせること）が、決して失敗することのない手品のように、常に完璧に機能すると主張していました。しかし、コンピュータはこう言いました。「ちょっと待ってください。これは特定の追加条件を加えた場合にのみ機能します」。形式化によって、この追加条件がなければ、その手品は失敗することが示されました。この論文は元の数学が無用であると言ったわけではありませんが、元の主張が広すぎたことを証明したのです。それは、「すべての鳥は飛べる」と言っていたら、ペンギンが存在することに気づいたようなものです。論文は、そのルールを真実にするために、「ペンギンの例外」を追加しなければなりませんでした。
2. 環と圏の混同： 論文はまた、これらの圏のルールを「可換環（commutative rings）」（一種の代数）のルールと比較しました。元の論文は、あるルールが両方に適用できることを示唆していました。コンピュータは、特定の、極めて小さな反例を見つけました。それは、わずか2つの対象といくつかの射を持つ小さな数学的パズルであり、そこではルールは環に対しては機能するものの、圏に対しては完全に崩壊していました。これは、自動車（環）を通すための橋のデザインが、自転車（圏）を走らせようとすると崩落してしまうことを発見したようなものです。論文は、これら二つの理論がこの点において同一であるという考えを明確に否定しています。

「余拡張（Codilatation）」のショートカット
この論文はまた、「余拡張（codilatation）」と呼ばれる巧妙なトリックを導入しています。逆方向（矢印が後ろ向きに進む方向）のルールを記述するために、新しいルールブックを一冊丸ごと書く代わりに、形式化は単にこう言いました。「地図を上下にひっくり返そう」。コンピュータが「左」と「右」を瞬時に入れ替える能力を利用することで、チームは新しい証明を一つも書くことなく、逆方向のルールを証明しました。これは、もしハンドルを反対に切れば、前進の運転方法を知っていれば、すでに後退の運転方法も知っていることになる、と気づくことに似ています。

結論
この論文は、「形式化された数学」の勝利です。それは拡張の理論が堅牢であることを証明しましたが、同時に品質管理検査官としても機能し、人間の目が見逃した元の理論の小さな亀裂を見つけ出し、修正しました。これは、複雑な数学をコンピュータが理解できる言語に翻訳すると、単なる検証が得られるだけでなく、数学そのものに対するより明確で精密な理解が得られることを示しています。論文は、理論は頑健ではあるものの、以前考えられていたよりも注意深い条件を必要とすることを結論づけており、将来誰かがこれらの「洗練された道路ルール」を使用したい場合に備えて、機械的にチェックされた完全な辞書を提供しています。