Has any previously unknown result been proven by an automated theorem prover?

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?


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.

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

Leave a Comment