全ての証明は有限長の記号列で記述できるとする。それは記号を文字コードで表すコーディングをすれば、
一つの巨大な二進整数になる。
また、ある命題Pに対する証明が存在するとすれば、それもまた非負の整数であるから、
非負整数の集合N＋から、その要素である整数ｎであってそのｎがPに対する証明の記述と
なっているものを取り出せば良い。数学命題に対する証明行為はそれで終わりになる。
そのようなｎが存在するならば、整数0から始めて1ではどうか2ではどうか3ではどうかと
1つずつｎを増やしてそれに対応する証明記述が存在して、Pの証明になっているかを
調べて行けば、Pの証明が存在するならばいつか必ずそれに到達できる。
しかしこれは猿にタイプライターを叩かせて、ハムレットの原稿ができてくるのを
待つような話である。しかし有限ステップで証明ができそうだろう。
証明の記述にはLEANによる表現を使っても良いわけだ。