8/13
3. AIは証明の本質を理解できるか？ 拡張版
田村「証明の本質を考えるなら、ブルバキ学派の『公理的数学』と、実験数学のアプローチを比較するべきだ。AIは形式主義の証明には適しているが、数学的な『発見』の本質は、意味の解釈にある。」
加瀬「例えば、ゲーデルの不完全性定理は、形式体系において自己言及が起こることで、完全な公理系が存在しないことを示した。これをAIが『理解』できるか？」
遠藤「今のAIは公理系の中で推論を行うが、ゲーデルのように『形式体系の限界そのもの』を考察することはできない。しかし、もしかするとAIが人間よりも適切な公理系を提案する未来はあるかもしれません。」
