The Robbins conjecture
historic
Sixty years no human could prove that Robbins' weak axiom yields Boolean algebra; in 1996 the EQP prover found the fourteen-step proof alone. The first machine-proved landmark theorem.