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! :)

Great tutorial, by the way!

There is another typo in one of the javascript functions, where you should write "return t;" instead of "return thm;"

Yes, this is in the definition of theorems().