Equivalent statements If one looks at the directed graph of all theorems proved, let there be a vertex between statement A and B directional if A implies B, ideally it will connect results across different fields. Is there any existing system, by computer or not, dedicated in looking into how existing proved theorems imply some otherwise not proved statements? Can one get access to it?
 A: In an unsatisfying sense, there already exists software for automatically deducing consequences of existing theorems.  Several automated theorem provers exist (see the list at Wikipedia), and I've used them in research from time to time.
But there is a catch: the vast majority of theorems are uninteresting.  Running this software blindly will simply result in a gigantic list of uninteresting theorems.
Let me illustrate:  When studying groups, Prover9 consistently gets bogged down in deducing a zillion theorems equivalent to the cancellation law or some other well-known identity.  Here's one random example (where * denotes the binary operation, e denotes the identity and ' denotes $^{-1}$):
x * (y' * (z * u')) != e | w * (u * (z' * (y * x'))) = w.

which says $$\forall w \forall u \forall x \forall y \forall z \quad\quad xy^{-1}zu^{-1}=\mathrm{id} \implies wuz^{-1}yx^{-1}=w.$$  A human would recognize this as a consequence of the group identity $(xy)^{-1}=y^{-1}x^{-1}$ and regard it as uninteresting.
Automated theorem provers are also more-or-less stuck with first-order logic (at least, for the time being), which is an enormous limitation.
However I'd like to note that they can be useful too, particularly if you want to prove millions of micro-theorems, which would be too tedious to do by hand.
