Mark_Friedenbach comments on Ganesalingam and Gowers on automated theorem-proving

[Mark_Friedenbach]

The size of the search space and lack of any reasonable heuristic.