Lisp による証明というのは興味深い
これは Lisp でなければならないのだろうか？

このようなことができるのなら，
不完全性定理の証明をある程度，視覚化できないのだろうか？