解説ねえ、智也くん！この論文の…
解説
ねえねえ智也くん！『LeanCat』っていう論文を見つけたんだけど、これって「痩せた猫」の研究なの？ダイエットかな？
いや、全然違う。それは『圏論（Category Theory）』っていう数学の分野を、Leanっていう証明アシスタントで扱うためのベンチマークの名前だよ。CatはCategoryの略だ。
えー、猫じゃないんだ、残念。でも「ベンチマーク」ってことは、AIのテストみたいなもの？
そう。今までのAIの数学テストは、パズルみたいなひらめき重視の問題が多かったんだ。でも、実際の現代数学はもっと抽象的で、過去の膨大な知識（ライブラリ）を使いこなす必要がある。この論文は、AIがそういう「抽象的な構造」をちゃんと扱えるか試そうとしているんだよ。
抽象的……。圏論って、電波の「圏内・圏外」とかの圏？
それは通信用語だろ。圏論は、数学的な構造そのものを扱う「数学の数学」みたいな分野だよ。例えば、集合とか群とか、異なる数学の世界に共通するルールを見つけるような学問だ。すごく抽象度が高いから、AIにとっても難しいんだ。
へぇー、数学の親玉みたいな感じだね！具体的にどんなテストをしたの？
100個の定理を用意して、それをAIに解かせたんだ。基本性質から「随伴（Adjunctions）」や「モナド（Monads）」っていう高度な概念まで、8つのトピックに分かれている。難易度もEasyからHighまで設定されているよ。
100問かぁ。最新のAIなら、サクッと全問正解しちゃったんじゃない？
それが、全然なんだ。一番賢いモデルでも、1回で正解できたのはたったの8.25%。4回挑戦させても12%しか解けなかった。特に難易度Highの問題は、どのAIも一問も解けなかったんだよ。
ええっ！そんなに低いの？AIって数学得意だと思ってたのに！
面白いのは、AIは「言葉での説明」はそれっぽく書けるのに、それをLeanっていう厳密なプログラミング言語みたいな形式に変換しようとすると、途端に失敗するんだ。これを「自然言語から形式言語へのボトルネック」と呼んでいるよ。
口では言えるけど、実際にやってみるとできない……。なんだか、夏休みの宿題を口先だけで終わらせようとする私みたいだね！
自慢することじゃないだろ。でも、この論文では『LeanBridge』っていう、ライブラリを検索してヒントを探す仕組みを使うと、少し成績が上がることも示している。AIが自分で知識を探しに行くのが大事なんだね。
なるほどね。これからAIがもっと賢くなれば、数学者さんのお手伝いができるようになるのかな？
その通り。このベンチマークは、AIがどれだけ人間に近づけるか測るための重要な指標になるはずだ。将来的には、もっと複雑な「2-圏論」とか、さらに高い次元の数学にも挑戦させる予定らしいよ。
すごい！じゃあ、いつかAIが「猫の気持ちを数学的に証明しました」なんて言う日が来るかも！
……それは圏論じゃなくて、ただの妄想だろ。いいから少しは勉強しろよ。
要点
- LeanCatは、数学の非常に抽象的な分野である「圏論（Category Theory）」に特化した、AIのための新しいベンチマークスイートである。
- 従来のAI数学ベンチマークはパズル的な問題が多かったが、LeanCatは現代数学で重要な「ライブラリを活用した抽象的な構造の推論」を評価する。
- 100個の形式化された定理（1-圏論）を含み、難易度はEasy、Medium、Highの3段階に分けられている。
- 最新の強力なAIモデル（ChatGPT-5クラスなど）でも、最も高い正答率で12%（pass@4）にとどまり、抽象的な数学推論の難しさが浮き彫りになった。
- 自然言語での証明はできても、それを厳密なコード（Lean）に落とし込む「自然言語から形式言語への変換」に大きな壁があることが示された。
- 検索機能を活用してライブラリを探索する「LeanBridge」という手法が、AIの性能向上に寄与することが確認された。