Similar nit, when you ask "Will theorems() discover `theorem halting_problem (n) : ¬ computable_pred (λ c, ..."

I don't believe it will since `const alphabet` does not contain λ or ¬. Apart from my very slight indignance after answering that one incorrectly, loved the article! :)