In enumerative combinatorics, a *bijective proof* that $|A\_n| = |B\_n|$ (where $A\_n$ and $B\_n$ are finite sets of combinatorial objects of size $n$) is a proof that constructs an explicit bijection between $A\_n$ and $B\_n$.
Bijective proofs are often prized because of their beauty and because of the insight that they often provide. Even if a combinatorial identity has already been proved (e.g., using generating functions), there is often interest in finding a bijective proof.


In spite of the importance of bijective proofs, the process of discovering or constructing a bijective proof seems to be an area that has been relatively untouched by computers. Of course, computers are often enlisted to generate all small examples of $A\_n$ and $B\_n$, but then the process of searching for a bijection between $A\_n$ and $B\_n$ is usually done the "old-fashioned" way, by playing around with pencil and paper and using human insight.


It seems to me that the time may be ripe for computers to search directly for bijections. To clarify, I do not (yet) envisage computers autonomously producing full-fledged bijective proofs. What I want computers to do is to search empirically for a *combinatorial rule*—that says something like, take an element of $A\_n$ and do $X$, $Y$, and $Z$ to produce an element of $B\_n$—that appears to yield a bijection for small values of $n$.


One reason that such a project has not already been carried out may be that the sheer diversity of combinatorial objects and combinatorial rules may seem daunting. How do we even describe the search space to the computer?


It occurs to me that, now that proof assistants have "come of age," people may have already had to face, and solve (at least partially), the problem of systematically encoding combinatorial objects and rules. This brings me to my question:



> 
> Does there exist a robust framework for encoding combinatorial objects and combinatorial rules in a way that would allow a computer to empirically search for bijections? If not, is there something at least close, that could be adapted to this end with a modest amount of effort?
> 
> 
> 


In my opinion, Catalan numbers furnish a good test case. There are many different types of combinatorial objects that are enumerated by the Catalan numbers. As a first "challenge problem," a computer program should be able to discover bijections between different kinds of "Catalan objects" on its own. If this can be done, then there is no shortage of more difficult problems to sink one's teeth into.



Automated search for bijective proofs
As mentioned in the comments, the [FindStat](http://findstat.org) 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.


1. 'automatically producing a bijection mapping one statistic to another' is demonstrated in [Two statistics on the permutation group](https://mathoverflow.net/questions/255252/two-statistics-on-the-permutation-group/255260#255260) and [Combinatorics problem related to Motzkin numbers with prize money I](https://mathoverflow.net/questions/278284/combinatorics-problem-related-to-motzkin-numbers-with-prize-money-i/278376#278376).
2. '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>.
3. 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.
4. 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.
5. I am also working on a new package that checks whether a statistic satisfying given constraints can possibly exist. But that's for later...


