Automated search for bijective proofs
As mentioned in the comments, the FindStat project is aiming at what you want. Concerning the size: it contains currently about 1000 'combinatorial statistics', that is maps $s:\mathcal C_n\to \mathbb Z$ on some (graded) set of 'combinatorial' objects $\mathcal C_n$ and about 150 'combinatorial maps' between two collections. What makes FindStat powerful is the (trivial) ability to compose maps. For example, for Catalan objects we obtain about 1.500.000 a priori different statistics.
Let me point out some possible ways of using it, in the spirit of the question.
'automatically producing a bijection mapping one statistic to another' is demonstrated in Two statistics on the permutation group and Combinatorics problem related to Motzkin numbers with prize money I.
'automatically producing conjectures' is achieved by clicking on 'search for distribution' on any of the statistics in the statistics database. The result is a list of statistics that are conjecturally equidistributed with the given statistic, but where a map transforming the first into the second might not be known. A classic is http://findstat.org/St000012.
it is easy to write a script that iterates 2. to find a 'partner' for a given pair of equidistributed statistics. An example is given in the comments to https://math.stackexchange.com/questions/2511943/leaf-labelled-unordered-rooted-binary-trees-and-perfect-matchings. Note that this meanwhile has a proof, also (essentially) discovered by FindStat.
a different kind of conjectures is provided by the list of 'experimental identities' found when selecting any of the maps at http://findstat.org/MapsDatabase. I am guessing that not all identities at http://findstat.org/Mp00101 are immediately obvious.
I am also working on a new package that checks whether a statistic satisfying given constraints can possibly exist. But that's for later...