This was far more than a brute force search. Thomas Hales did a talk about the proof and during the QA he mentioned that the proof was improved a lot as part of

This was far more than a brute force search. Thomas Hales did a talk about the proof and during the QA he mentioned that the proof was improved a lot as part of formalizing it into HOL. The process even lead to solutions of other problems [1]. 1: http://youtu.be/DJx8bFQbHsA?t=40m57s http://youtu.be/DJx8bFQbHsA?t=40m57s