3 ms·
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
by shmageggy 10y ago
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?
- deleted 10y ago[deleted]
- deleted 10y ago[deleted]
- ikeboy 10y agoProofs 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.
- deleted 10y ago[deleted]
- shmageggy 10y agoIt's not letting me reply any deeper, but that makes sense, thanks!
- wging 10y agoI think it's that you can't reply to posts that are too new.
- tomjakubowski 10y agoYou 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 https://news.ycombinator.com/item?id=11750351
- wolfgke 10y agoThe 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 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).