Bob Veroff has a few examples of results that I believe many would find interesting, first proved by a computer, such as relatively short single axiom bases for Boolean Algebra. Though, not all of what he proves there makes for a new result.
A perhaps better example consists of the proof of XCB as one of the shortest single axioms for the classical equivalential calculus under E-detachment (from, E$\alpha$$\beta$, as well as $\alpha$, we may infer $\beta$). The proof of XCB, in effect, completed the solution of what one might think of as the larger problem. The larger problem here can get stated as:
"Find all of the shortest axioms, up to re-lettering of variables, under E-detachment for the classical equivalential calculus."
Many similar larger problems in logic (and probably also abstract algebra) remain open. I note that Ulrich's site doesn't have a complete list of these problems (this is not to get blamed on Ulrich)... for instance the problem of finding the set of the shortest single axioms for classical propositional calculus in disjunction "A", and negation "N" under A-N detachment "From AN$\alpha$$\beta$, as well as $\alpha$, infer $\beta$", remains open.