ねぇ、誰も言及してないっぽいから言っとくけど、チューリングマシンって乱数とか無いぢゃん？
個人的には量子論的な乱数の存在がゲーデルさん的な「人間はコンピュータよりつおい」の根源的原因かもと思うのさ。
でさ、時刻とかカーソルの動きとか様々な外部要因を取込んで強化したぎじ乱数を、ぎじでもいいから使うべきだと思う。
既に与えてある定理の一部の文字をランダムに取換とか改変し、その文が論理的に正しい文になるまで取換や改変、を続けさせるとか。
与えられた語彙の中からランダムに定義行為や公理設定行為を行わせてみるとか。