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?

**Answer**

Robbins’ conjecture that all Robbins algebras are Boolean algebras was first proved using EQP, after Tarski and others had tried and failed to prove or disprove it.

**Attribution***Source : Link , Question Author : shamp00 , Answer Author : joriki*