The Wikipedia page on automated theorem proving states:
Despite these theoretical limits, in practice, theorem provers can solve many hard problems…
However it is not clear whether these ‘hard problems’ are new. Do computer-generated proofs contribute anything to ‘human-generated’ mathematics?
I am aware of the four-color theorem but as mentioned on the Wikipedia page, perhaps it is more an example of proof-verification than automated reasoning. But maybe this is still the best example?