Accompaniment to the essay on Godel Numbers : )
Handy functions that encode "PM-Lisp", into Godel Numbers and vice versa.
This just works for formulas -- most proofs would be too big to even fit in a biginteger!
(pm-lisp->godel-num '(next 0))
(godel-num->pm-lisp 4688381250N)