[FOM] Automated bijective proofs

[Timothy Y. Chow]

I wonder if there has been any effort to automate the process of finding 
bijective proofs in combinatorics?

Pace Littlewood, not all identities are trivial.  Combinatorialists spend 
a fair chunk of their time trying to find bijective proofs of identities,
including identities for which proofs by other means (linear algebra,
algebraic geometry, representation theory, analysis, ...) are already
known.  I will not try to define "bijective proof" but it generally has
the flavor of finding natural combinatorial interpretations for both sides 
of the identity and explicitly constructing a bijection between the two 
sets of combinatorial objects.

So far as I am aware, finding bijective proofs remains a black art, 
requiring all the human ingenuity and creativity for which the best 
combinatorialists are renowned.  However, the striking thing from my
point of view is that many bijective proofs are in some sense variations
on a few basic themes.  Therefore it seems to me that if these themes
were articulated precisely, then computers could rapidly search the
space of possible (or at least plausible) bijections, and if not generate
a rigorous proof directly, at least generate maps that the numerical 
evidence would suggest are bijections.

The project of precisely articulating the types of constructions used
in bijective proofs is an ambitious one because the methods used by
working combinatorialists are (on the surface at least) extremely
diverse.  However, it does not seem to me to be completely out of
reach, especially if the domain is suitably restricted at first.

More importantly, in the spirit of the message that Harvey Friedman
repeatedly emphasizes---that more needs to be done to attract the
working mathematician to the importance of foundational work---if
the project of automating bijective proofs is successful, it would
certainly capture the attention of working combinatorialists.  The
success of the Wilf-Zeilberger methods of proving hypergeometric
identities illustrates this fact; nobody working with hypergeometric
functions or identities can afford to ignore the tremendously powerful
automated proof techniques that have been found.

I can give some more specific thoughts on particular types of bijections 
if anyone is interested.

Tim