I thougut this article was going to be about Appel and Haken's proof of the Four Color Theorem, as it was the first to use software and not an actual analytical proof. As a result mathematicians were split: while this proof may have shown the theorem was true, it didn't explain why it was true. Because the latter was reduced to a brute force search.

https://math.stackexchange.com/questions/23409/did-the-appel...