証明すべき命題をどう符号化するか、という問題がまずある。
もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか？
そんなアルゴリズムが果たして存在するのか？