AI支援形式証明への道報告-3 圏論のプラグイン化 - 檜山正幸のキマイラ飼育記 (はてなBlog)

「AI支援形式証明への道」を書いた頃（2025年11月末）から、AIチャットボットに手伝ってもらって、Lean 4 により定義や定理を記述することを試しています。

今のAIは高性能で速いですが、それを使っている僕が低性能で遅いので、全体の進捗は「遅々としている」と言わざるを得ません。しかしそれでも、少しは話が進んでいます。今（2025年の年末）、AIチャットボットと Lean 4 でやっていることは、「代数系達の圏にプラグインを追加して拡張*1するメカニズム」の定義です。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\twoto}{\Rightarrow}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\o}[1]{\overline{#1} }
\newcommand{\u}[1]{\underline{#1} }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
`$

内容：

最近の状況
多元環達の圏
代数的形容詞
マグマから派生する代数系達
プラグインとミクシン
AIとの共同作業

ハブ記事：

AI支援形式証明への道報告-1

多元環達の圏

「多元環」とは、英語の "algebra" の翻訳語です。直訳すれば「代数」です。しかし、「代数」という言葉は曖昧多義語です。

代数学という分野
一般的な代数系／代数構造
加群に掛け算（双線形写像）を載せた代数系

3番目の意味の "algebra" の翻訳語（意訳）が「多元環」です。

多元環の掛け算〈積〉に、結合法則や単位法則を仮定することがありますが、ここでの多元環では、何の仮定も設けません。単なる双線形写像が掛け算〈積〉です。何の仮定（法則）もないことを強調して、一般多元環〈generic algebra〉とも呼ぶことにします。

一般多元環達の圏を $`\mbf{GenAlg}_R`$ とします。ここで、下付きの $`R`$ は可換環です。一般多元環は加群を台〈underlying object | carrier〉とする代数系ですが、加群には係数環〈スカラー環 | 基礎環〉があります。$`R`$ は台加群の係数環です。

掛け算に対する仮定（法則）が入った多元環達は、それぞれ固有な圏を形成します。

$`\mbf{AssocAlg}_R`$ ：結合的多元環達の圏
$`\mbf{UnitalAssocAlg}_R`$ ：単位的・結合的多元環達の圏
$`\mbf{LieAlg}_R`$ ：リー代数達の圏

これらの圏は、一般多元環に法則を追加して得られた多元環達の圏です。

単に法則の追加だけでなくて、構造の追加も必要となることもあります。次のような圏は、一般多元環に構造（と法則）を追加して得られる多元環達の圏です。

$`\mbf{GradedAlg}_R`$ ：階付き多元環達の圏
$`\mbf{ExterAlg}_R`$ ：外積多元環達の圏
$`\mbf{CliffordAlg}_R`$ ：クリフォード代数達の圏

代数的形容詞

いま、$`\mrm{assoc}, \mrm{unital}, \mrm{lie}`$ などの名前〈ラベル | タグ〉を考えます。これらは、多元環〈algebra〉に付く形容詞を表しています。多少の短縮をするときもあり、全部小文字の語にしてますが、それは構文的な約束ごとで本質的ではありません。

様々な多元環は、形容詞付きの名詞で表現できます。次のようです。

associative algebra
unital associative algebra
Lie algebra

これを、$`\mbb{Alg}_R`$ という親語に、形容詞を後置する構文で書くことにします。

associative algebra は $`\mbb{Alg}_R[\mrm{assoc}]`$
unital associative algebra は $`\mbb{Alg}_R[\mrm{unital}, \mrm{assoc}]`$
Lie algebra は $`\mbb{Alg}_R[\mrm{lie}]`$

ここに出てきた $`\mbb{Alg}_R[\mrm{assoc}]`$ 、$`\mbb{Alg}_R[\mrm{unital}, \mrm{assoc}]`$ 、$`\mbb{Alg}_R[\mrm{lie}]`$ は、それぞれ対応する多元環達の圏を表すとします。つまり：

$`\mbf{AssocAlg}_R = \mbb{Alg}_R[\mrm{assoc}]`$ ：結合的多元環達の圏
$`\mbf{UnitalAssocAlg}_R = \mbb{Alg}_R[\mrm{unital},\mrm{assoc}]`$ ：単位的・結合的多元環達の圏
$`\mbf{LieAlg}_R = \mbb{Alg}_R[\mrm{lie}]`$ ：リー代数達の圏

このように考えると、$`\mbb{Alg}_R`$ は、形容詞のリストを引数として多元環の圏を構成するコンストラクタということになります。コンストラクタ $`\mbb{Alg}_R`$ に渡す形容詞を特に代数的形容詞〈algebraic adjective〉と呼ぶことにします。algebraic は多元環的という意味でもあるので、多元環形容詞でもかまいません。文脈から明らかなら単に形容詞〈adjective〉とも呼びます。

法則を追加する意味を持つ形容詞の場合は、その形容詞で修飾された多元環の圏を構成するのはそれほど難しくありません。しかし、形容詞 $`\mrm{graded}`$ 、$`\mrm{exter}`$ 、$`\mrm{clifford}`$ などは追加の構造も必要なので構成は複雑になります。

マグマから派生する代数系達

前節で説明したコンストラクタ $`\mbb{Alg}_R`$ と代数的形容詞を、Lean でいきなり実装するのはハードルが高いので、単純化したバージョンをサブゴールに選びました。可換環上の加群の代わりに単なる集合を使うバージョンです。

単なる集合上に、何の法則も持たない掛け算〈積〉が載った構造はマグマ〈magma〉と呼びます。マグマは、一般多元環の集合バージョンになります。言い方を変えるなら、一般多元環は、マグマの加群バージョンです。

圏コンストラクタ $`\mbb{Mag}`$ に代数的形容詞を渡して様々な“代数系の圏”を構成します。代数的形容詞としては、次のようなものを考えます。

$`\mrm{assoc}`$ : 二項演算〈積〉が結合的であることを表す形容詞
$`\mrm{pointed}`$ : 特定された点〈distinguished point〉を持つことを表す形容詞
$`\mrm{unital}`$ : 二項演算が単位的であることを表す形容詞
$`\mrm{comm}`$ : 二項演算が可換であることを表す形容詞

ここで、$`\mrm{unital}`$ は $`\mrm{pointed}`$ を要求〈require〉するとします。つまり、単位法則の単位元として特定された点が必要になる、ということです。

$`\mrm{assoc},\mrm{unital},\mrm{comm}`$ は、法則を仮定する形容詞ですが、$`\mrm{pointed}`$ は（特定された点という）構造を追加します。法則を仮定する形容詞と構造を追加する形容詞では、性格が違います。

圏コンストラクタ $`\mbb{Mag}`$ に代数的形容詞のリストを渡すと、次のような圏が構成できます。

$`\mbf{Magma} = \mbb{Mag}[\;]`$ ：マグマ達の圏
$`\mbf{Semigrp} = \mbb{Mag}[\mrm{assoc}]`$ ：半群達の圏
$`\mbf{PtMagma} = \mbb{Mag}[\mrm{pointed}]`$ ：付点マグマ達の圏
$`\mbf{Mon} = \mbb{Mag}[\mrm{assoc},\mrm{pointed}, \mrm{unital}]`$ ：モノイド達の圏
$`\mbf{CMon} = \mbb{Mag}[\mrm{assoc}, \mrm{pointed},\mrm{unital}, \mrm{comm}]`$ ：可換モノイド達の圏

プラグインとミクシン

今まで述べたアイディアを、Comet（AIチャットボット）に伝えるために、ソフトウェアのプラグイン・アーキテクチャに似ていると説明しました。また、オブジェクト指向のミクシン〈mixin〉／フレーバー〈flavor〉にも似ている、とも。こういう比喩や類似性による説明は、AI相手にもけっこう有効です。

Comet は、Lean のライブラリでもミクシンは使われているという情報を拾ってきたので、Lean におけるミクシン手法を使うことにしました。僕が「Lean におけるミクシン手法」を知っているわけではないのですが、Comet が言うことをとりあえず信じてみた、ということです。「Lean におけるミクシン手法」がハルシネーションだったら失敗しますが、そんときはそんとき*4。

ベースとなる代数系であるマグマに、プラグイン〈アタッチ | インジェクト〉するミクシンとして $`\mrm{Assoc}`$ 、$`\mrm{Pointed}`$ などがあり、ミクシンのタグ〈ラベル〉が形容詞 $`\mrm{assoc}`$ 、$`\mrm{pointed}`$ などです。“形容詞＝ミクシンタグ”とミクシンは一対一対応します。ミクシン自体は、Lean の型クラス（ミクシンクラス）で実装します。

圏コンストラクタ $`\mbb{Mag}`$ の実装である Lean のコンストラクタ関数は、“形容詞＝ミクシンタグ”からミクシンクラスをルックアップして、マグマの定義に混ぜ込んでゴニョゴニョします。ゴニョゴニョした結果は圏なので、Category という型のインスタンス*5です。

どうやってゴニョゴニョするかが問題で、現在試行錯誤中です。

AIとの共同作業

AIとの共同作業は、人間との共同作業とそんなに変わるわけじゃないです。任せられるところは任せて、注意は怠らない、ということです。

意図をちゃんと伝えれば、難しいことでもやってくれると信じる。
ときに、早とちり（プロンプトの誤認）や間違い（ハルシネーション）をしでかすから、その点は注意。

コピペのような雑用は全部僕の担当なのがちょっと悲しいです*6が、いずれは改善されるでしょう。

*1:[追記]「拡張」という言葉は誤解をまねくかも知れません。圏を大きく膨らませることではなくて、もとの圏への忘却関手を持つ新しい圏を作ることです。[/追記]

*2:ハルシネーションが疑われるときは、同じ質問を Comet と Edge Copilot に投げて比較しています。同じ嘘をつかれる可能性も皆無ではないですが。

*3:AIは、人の悪口は言わないようにトレーニング／チューニングされているようです。しかし、相手が人でないとあまり抑制が効かないようで「AIがAIの悪口を言う」ことはあります。AIにはシコファンシー〈Sycophancy | おべっか | へつらい〉という特性もあるので、ユーザーである僕にウケると思って言っている可能性もあります。

*4:難しい課題を与えると、AIはあたかも（印象・雰囲気としては）「自分が知らない／出来ないのをごまかす」ように嘘をつきます。ハルシネーションにいちいち怒っていては精神衛生上よくないので、「優秀でいいヤツだが虚言癖がある」と思って付き合ったほうがいいです。

*5:[追記]「インスタンス」も要注意な用語です。「型クラスのインスタンス」というと、型クラスに登録されたインスタンスの意味です。登録とは無関係な場合は「住人〈inhabitant | habitant（仏語）〉」というほうがいいかも知れません。[/追記]

*6:[追記]零細企業の社長が、ごみ捨てやトイレ掃除を全部引き受けているような感じです。[/追記]

最近の状況

多元環達の圏

代数的形容詞

マグマから派生する代数系達

プラグインとミクシン

AIとの共同作業