Yes, absolutely, this is an amazing win, and I say that as someone who studied math at the graduate level. The more drudgery we can offload to the computer, th

Yes, absolutely, this is an amazing win, and I say that as someone who studied math at the graduate level. The more drudgery we can offload to the computer, the better it is for everyone. In this case, though, the computer actually provided the equivalent of creative thought, leading to new directions toward a proof. Personally, I've been looking around for resources on driving a proof assistant (Lean is my current favorite) using a scripting language. If anybody happens to know of any pre-made libraries that do that, preferably in Python or Ruby, that would be awesome.