ChatGPTと数学

いくつか聞いてみたんですが、Referenceがでたらめってのは、置いといて...

推論はしてくれないので、知ったかぶりレベルなんだよな。で、自分でもそうなんだけど、

　数学の本は、おれおれ定義と用語で突っ走ってるのが普通

その中では閉じてるわけ。それで合ってるのが、むしろ不思議なレベル。なので話が合わない。

数学は異なる視点があって、例えば線形代数は集合でもあるし群でもあるし圏でもある。そういうのがだめらしい。

話は合わせてくるんですが、その先にあるモデルがない感じ。まぁ、ないものねだりしてもしかたないが。

じゃぁ、Agda ではどうなのかというと、

　　字面の証明の後ろには、かなり複雑な証明のλ項がある
　　それは数ギガの大きさを持つことがある

つまり、モデルを表す巨大なデータ構造があるらしい。それは、LLMそのものだとも思うんですが、

　　AIがLLMそのものを扱えるのか
　　数学者はそもそも、その数ギガの記号モデルを扱っているのか

あたりが面白いかな。

質問の仕方が悪いと「意味がない」とか言ってきて面白いです。

Q 商群の定義は普遍問題だったりする?

A 商群の定義は、実際には余普遍性に関連する問題です。群 G とその正規部分群 N が与えられたとき、商群 G/N は、以下の余普遍性を満たすものとして定義できます。

π は G から G/N への射であり、N をその核にもつ準同型写像である（すなわち、π(n) = 1_G/N となる任意の n ∈ N）。
任意の群 H と G から H への準同型写像 f で、N を核にもつものが存在する場合、一意の射 g: G/N → H が存在して、f = g ◦ π となる。