# [FOM] Computer searches for combinatorial bijections

Timothy Y. Chow tchow at alum.mit.edu
Wed Feb 28 10:47:44 EST 2007

```I'm picking up this old thread from a few months ago, because I have a
small additional insight.  Mitchell Harris reminded me that I broached the
same topic ("Automated bijective proofs") back in 2004.

On Wed, 11 Oct 2006, Jacques Carette wrote:
> The framework of species gives one a lot of canonical maps and tools
> between species, which help tremendously in the automation of possible
> bijections.

Having just finished a paper in which I constructed a couple of nontrivial
bijections between sets of lattice paths in the plane---partly aided by
what seems to be involved here.

Canonical maps are certainly important, and categories/species are
certainly helpful as a language for them.  However, when a
combinatorialist seeks an *explicit bijection*, usually this is something
decidedly *non-canonical*.  The (verbal) description of the bijection
typically involves some non-canonical choices, e.g., "pick the first node
with such-and-such a property and then..."  Another way to put it is that
one attaches labels to unlabeled structures, or one tries to "remember"
what some forgetful functor forgot.

In my lattice-path example, I had conjectured that two sets of lattice
paths were equinumerous.  I derived a generating function equation from
the conjecture, manipulated it to an equivalent but different-looking
form, and then stared at it, asking, "What are these terms counting?"
Using intuition or guesswork or whatever you call it, I eventually
constructed the appropriate combinatorial structure that allowed the
bijection to be constructed.  Given the structure, passing to the
generating function was a functorial forgetting process, but finding the
proof required going in the opposite direction.

Therefore what an automated search for candidate bijections needs to do is
to try a bunch of "possible labelings" of the given objects and look for
canonical maps between the tentatively labeled objects.  The space of
possible labelings is vast and hence a lot of thought needs to go into the
problem of structuring this space so that it can be explored fruitfully.
However, if this hurdle can be surmounted then potentially a computer can
search the space much better than an unaided human can.

To make further progress I think one needs to fix a toy domain that is
relatively well understood and that one can play with concretely.  I'm not
sure what a good candidate would be.

Tim Chow
```