On: The Busy Beaver Game

[shmageggy]

Yeah a bit. This part

> searches for a proof in ZFC (or your favorite alternative)

is tripping me up though. It's not obvious to me that you can do this in an automated fashion. I assume this is a standard tool for theorists though? How does such a program work?

[wolfgke → shmageggy]

The idea is that proof systems can be formulated as a grammar for a recursively enumerable language (Type 0 grammars in the Chomsky hierarchy): https://en.wikipedia.org/wiki/Chomsky_hierarchy#Summary, such that if there is a proof of a particular statement a corresponding word can be derived by the corresponding grammar. But this can easily be done by a Turing machine (either check through all possible derivations in the grammar or, more abstract, let the Turing machine let non-deterministically choose a possible derivation and use the fact that the expressiveness of non-deterministic Turing machines is the same as for deterministic Turing machines).

[shmageggy → shmageggy]

It's not letting me reply any deeper, but that makes sense, thanks!

[wging → shmageggy]

I think it's that you can't reply to posts that are too new.

[tomjakubowski → wging]

You can, you just have to click on the timestamp to visit the comment's item page first, something like https://news.ycombinator.com/item?id=11750351

[ikeboy → shmageggy]

Proofs can be expressed using a string and verified to check every step is valid.

So brute force over every string, checking if it's a valid proof for the claim you want.