There are a lot of parallels between rule-based games like Go and rule-based formal systems like ZFC. It’s interesting that the same techniques used for AlphaGo have not worked nearly as well for finding proofs of famous open problems that we suspect are both 1) decidable within ZFC and 2) have a “reasonable” minimal proof length.

What aspect of efficiently exploring the combinatorial explosion in possibilities of iterated rule-based systems is the human brain still currently doing much better than machines?