This is really excellent. Amazing how much clearer the author’s Lisp code makes things (even to a non mathematician and non lisper). It’s rare to find explanations of difficult topics that are this well communicated, but I hope it becomes a trend.
I agree and I want to add that I particularly appreciated how you consistently, in programming terms, communicated the type of things. Eg:
(proves a b)
So far saying “the sequence with the Gödel Number a proves the formula with Gödel Number b”
In my experience, most mathematicians would have instead written "So far saying 'a proves b'". Repeating the type of the parameters consistently made it significantly easier for me to follow along. I hope this becomes more common.
