まず宣伝から始めさせていただきます．
9/3 に，「数学系のためのLean勉強会」が開催されます．
最近数学界隈で話題沸騰中のLean言語のことが学べます．予備知識として数学科の学部２年程度の内容が仮定されるので「高校までしか数学を習っていない」という人向けではないですが，そうではない方はぜひご参加ください．
対面参加は定員に達したので締め切られていますが，オンライン参加はいまでも受付中だそうです．
…私はこのイベントの関係者でもなんでもないのですけどね．にぎわってほしいので，ぜひ参加してください．
さて今回の本題ですが，Lean で圏論をやるとき，図式を見ずに射の合成を追っていく必要がありますね．
たとえば，次のようなコードがよく出てきます．一番下の行が示すべきことで，それより上の行は仮定として得られていることです．>> は射の合成です．
正直みづらいですが，文字列を操作することしかできない証明アシスタントでは，これを頑張って解読するしかなさそうに思えます．
しかし Lean4 はカスタマイズ性が高く，ユーザが独自にウィジェットを作って infoview の表示をカスタマイズすることができます．この場合，CommDiag というウィジェットがありまして，それでたとえばゴールの図式を可視化することができたりします．*1
すごいですね！infoview は React のような構文で書かれているらしいですよ．
このように拡張性が高いというのは，Lean4 が単なる定理証明支援系ではなくて「プログラミング言語」であるということのうま味であるといわれます．今回は図式でしたが，グラフを表示したりすることもできるようです．楽しいですね．
今回紹介したこの CommDiag ウィジェットのサンプルコードはこちらにあります：
ぜひ確かめてみてください．
*1:正確には Lean4 ではなくて mathlib4 の機能です
