Have automated theorem provers proved anything we didn't already know? (math.stackexchange.com)