Automated theorem provers can't prove this problem. Which non-trivial Math problem you think are thougher than this Erdos problem?