Thanks for posting this. This approach certainly seems like the most straightforward way to test systems. “Here are unacceptable ideas and some desirable ideas. Does this system generate the desirable ones and not the unacceptable ones?” The problem is that this isn’t computationally reasonable, at least not generally. We could do it with tricks, though someone would have to develop those tricks first :)
I wonder what principles would lead a robot to create that list of unacceptable theorems?
Thanks for posting this. This approach certainly seems like the most straightforward way to test systems. “Here are unacceptable ideas and some desirable ideas. Does this system generate the desirable ones and not the unacceptable ones?” The problem is that this isn’t computationally reasonable, at least not generally. We could do it with tricks, though someone would have to develop those tricks first :)
I wonder what principles would lead a robot to create that list of unacceptable theorems?
Thanks for this comment—it helped clarify to me what exactly the paper was doing.