数学界とAIの問題。意味のある証明、群論などの理論が途中で出来るという話。私の場…

jrf> 数学界とAIの問題。意味のある証明、群論などの理論が途中で出来るという話。私の場合はラムダ計算の証明において人間にわかりやすい証明が自動証明では「効率的」でないという形で現れた。「わかりやすい証明」が評価されがたい。しかし、命題の表現力を高めて人間にフレンドリーにする…例えばオブジェクト指向を使って…などの必要性はあると私は考えていた。その過程で「わかりやすい証明」にも意味が出るだろう…と。実際は、命題の表現力を高めるより、人間がコンピュータの記号に慣れるような方向に行った気がする。どちらかというと。