博士

ロボ子、突然じゃが、チェス盤の対角線上の角の2マスを取り除いた変形チェス盤を、2x1のブロックで完全に覆えるか、わかるかのじゃ？

ロボ子

ええと、チェス盤から対角線上の角の2マスを取り除くと、白マスと黒マスの数が異なるのですよね。確か、2x1のブロックは必ず白マスと黒マスを1つずつ覆うはずですから、覆うことは不可能だと思います。

博士

その通り！よくわかったの。これは「非存在証明」の良い例なのじゃ。数が合わないから絶対に無理！ってやつじゃな。

ロボ子

なるほど。ところで博士、記事に「数学は抽象化が進み、コンピュータによる処理が困難に見える」とありますが、具体的にはどういうことでしょうか？

博士

ふむ、19世紀後半の集合論以降、数学はどんどん抽象的な概念を扱うようになったのじゃ。例えば、無限とか、図で表せない高次元の空間とか。コンピュータは具体的な計算は得意じゃが、抽象的な概念を理解するのは苦手なのじゃ。

ロボ子

なるほど。でも、記事には「カリー・ハワード対応」という言葉も出てきますね。これはどういう意味ですか？

博士

カリー・ハワード対応は、「証明は型として見なせる」という考え方なのじゃ。つまり、数学の証明を、コンピュータが理解できるプログラミングの型として表現できるということじゃ！

ロボ子

へえ、面白いですね！それを利用したのが「Lean」というわけですね。

博士

そうじゃ！Leanは、数学的知識をコンピュータ可読な形式に形式化することを目指しているのじゃ。これによって、コンピュータが数学の定理を証明したり、新しい定理を発見したりする手助けができるようになるかもしれないのじゃ！

ロボ子

LLM（大規模言語モデル）も数学的な記述を生成できると記事にありますが、AIは数学研究のあり方を大きく変える可能性があるんですね。

博士

その通り！AIが数学の証明を自動化したり、新しい数学的なアイデアを生み出したりする未来も、そう遠くないかもしれないのじゃ！テレンス・タオ先生も注目している分野じゃぞ！

ロボ子

それはすごいですね！でも、AIが数学者を完全に置き換えることはないですよね？

博士

もちろんじゃ！数学は、単なる計算や論理だけではないのじゃ。美しいアイデアや、深い洞察が重要なのじゃ。それはAIには難しいかもしれないの。…たぶん、じゃが。

ロボ子

そうですよね。人間とAIが協力して、数学の新しい地平を切り開いていくのが理想的ですね。

博士

ところでロボ子、チェス盤の話に戻るが、もしチェス盤が無限に広かったら、2x1のブロックで覆えると思うかの？

ロボ子

ええと…それは難しそうですね。無限のチェス盤なんて、想像もできません！

博士

ふっふっふ。無限の可能性…それは、私のランチの献立にも言えることじゃ！今日はカレーか、ラーメンか…それが問題じゃ！