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.