It should be noted that there is some reason to aesthetically dislike computer-generated proofs.
It's not mentioned by Baez, but one of the first breakthroughs in the Erdos discrepancy problem was a very verbose (running into a few GBs if I remember right), computer generated proof, for a subcase. Terry Tao later presented a general proof which was far far shorter.
Obviously there are cases like the 4-color theorem which have withstood the test of time and prejudice, but there is something sad about not being able to make sense of such math.
It's not mentioned by Baez, but one of the first breakthroughs in the Erdos discrepancy problem was a very verbose (running into a few GBs if I remember right), computer generated proof, for a subcase. Terry Tao later presented a general proof which was far far shorter.
Obviously there are cases like the 4-color theorem which have withstood the test of time and prejudice, but there is something sad about not being able to make sense of such math.