"METAMATHEMATICS, MACHINES, AND GOEDEL'S PROOF" N.Shankar SRI International
で、ゲーデルの不完全性定理をLispで書いてるけど、ってことは形式化されてる
ってことだよね。