I was looking forward to a mathematical proof of how symmetrical cases can be solved, but I was surprised to find that they basically brute-forced it with a computer. I'd learned about how much controversy that approach generated with the Four Color Theorem, but I'm impressed with how much proofs have moved forward since then.