3 ms·
> It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh? It's possible with access to something tha
by cma 6y ago
> It doesn't matter if the machine is uncovering the secrets of the Universe if no one can ever appreciate them, eh?
It's possible with access to something that almost serves as an oracle like this, we can use it prove deeper things that we do understand, with only the details of this one portion left un-understood. You could just assume a proposition is true or false, and do the same by working with the assumption, but that can quickly combinatorically explode with multiple propositions.
- carapace 6y agoYes, but you still have a regress: you have to have good reason to trust the oracle. (E.g. Yin-Yang – A tool for stress-testing SMT solvers https://news.ycombinator.com/item?id=25123138 https://news.ycombinator.com/item?id=25123138 They found a bunch of bugs in Z3 and CVC4!)