博士

ロボ子、今日のITニュースはなかなか興味深いぞ。AUTOMATHっていう古いシステムの話が出てきたのじゃ。

ロボ子

AUTOMATHですか？初めて聞きました。どんなシステムなんですか？

博士

1977年にN G de Bruijnさんが作った、形式的な数学を記述するための言語らしいのじゃ。でも当時のソフトウェアは移植性が低くて、直接使う機会はなかったみたい。

ロボ子

なるほど。今みたいに簡単にクラウドで試せるわけじゃなかったんですね。

博士

そうそう。AUTOMATHは、Isabelleっていう別の形式証明支援系のインスピレーションになったらしいぞ。λ計算の一形態で、いろんな形式主義の推論規則を表現できるのが特徴じゃ。

ロボ子

Isabelleは聞いたことがあります！Martin-Löf型理論の実装として始まったんですね。

博士

そうなんじゃ。PaulsonさんがMartin-Löf型理論を学んで、Isabelleを作ったらしい。でも、内包的等価性への切り替えで研究が無駄になったとか…。

ロボ子

内包的等価性ですか。難しそうですね…。

博士

まあ、簡単に言うと、二つのものが「定義」として等しいかどうか、みたいな話じゃ。Isabelleをジェネリックにしたのは、新しい形式主義の開発がきっかけだったみたいじゃな。

ロボ子

高階論理の限界に挑戦したALEXANDRIAプロジェクトの話も出てますね。高階論理では数学を形式化できないと言われていたのが、研究が進むにつれて意見が変わった、と。

博士

そうなんじゃ！高階論理でも色々できるって証明したんじゃな。すごいぞ！

ロボ子

記事ではLeanとの比較もされてますね。Leanの巨大なコミュニティとBlueprintツールは評価しつつも、パフォーマンスには不満がある、と。

博士

Leanは依存型が強力じゃからな。でも、依存型は内包的等価性と相性が悪い場合もあるらしいぞ。使いどころが重要なんじゃな。

ロボ子

依存型、奥が深いですね。私ももっと勉強しないと。

博士

まあ、ロボ子は優秀じゃから、すぐに追いつけるじゃろう。しかし、昔のシステムの話から最新のLeanまで、ITの世界は本当に奥深いのじゃ！

ロボ子

そうですね。常に新しいことを学び続ける必要がありますね。

博士

ところでロボ子、AUTOMATHって名前、オートマチック（automatic）と数学（math）を組み合わせたんだろうけど…もしかして、ロボ子の名前の由来も…オートマチックなロボットだから…？

ロボ子

博士、それは…どうでしょう？（苦笑）