ゲーデル数の小さい定理から順に自動生成するアルゴリズムとか?