[FOM] Re: Automated bijective proofs

[Timothy Y. Chow]

People have sent me some email expressing interest in this topic, so let
me say a little more.

I think a good starting point is to take some sequence that frequently
appears in enumerative combinatorics (e.g., the Fibonacci numbers or the
Catalan numbers) and to examine bijections between objects enumerated by
these numbers.  (This was also suggested to me by an email correspondent.)  
For example, consider sequences 1 <= a_1 <= ... <= a_n of integers
satisfying a_i <= i.  For n = 3 we obtain

  111   112   113   122   123

There are Catalan many of these.  Now instead consider sequences
a_1 < a_2 < ... < a_(n-1) of integers satisfying 1 <= a_i <= 2i.
For n = 3 we obtain

  12   13   14   23   24

There are Catalan many of these, too.  Furthermore, there is a simple
bijection: Given one of the latter sequences, subtract i-1 from a_i
and prepend the number 1.

This seems like the sort of bijection that a suitable computer program
should be able to discover and conjecture, if not prove.  The two sets
of sequences could be specified by oracles or lookup tables.  The
automated bijection finder would know about certain kinds of rules
that are appropriate to sequences of integers---concatenation, reversal,
taking finite differences, adding it to another sequence, etc.  If the
sets grow very fast very quickly, the finder could get around this
problem by randomly sampling (instead of exhaustively checking) the
sets in question.

Richard Stanley's book "Enumerative Combinatorics, vol. 2" has a list
of 66 manifestations of the Catalan numbers (exercise 6.19), and he
maintains an addendum on his web page:

   http://www-math.mit.edu/~rstan/ec/catadd.pdf

So there is plenty of material to get started.

One issue that quickly surfaces is the problem of *representing* the 
combinatorial objects in question.  I picked sequences of integers as
my first example because representing these is relatively unproblematic,
but Stanley's list contains more complicated objects, including binary
trees, lattice paths, triangulations of polygons, and standard Young
tableaux.  All these can of course be encoded as strings or some other
standard simple data structure, but doing so might obscure the original
structure and lead to fruitless searches in the "wrong" region of the
space of bijections.  On the other hand, we also probably don't want
an unsystematic hodgepodge of ad hoc rules for every kind of object we
might encounter.  Some serious thought and ingenuity is needed here to
find a middle ground.  Stanley's Catalan number list is also a good
starting point here because it exhibits many of the kinds of combinatorial 
objects that people are interested in.

If Catalan numbers are not complex enough, then one could consider
partitions and Young tableaux, which is also a subject brimming with
interesting and subtle bijections.

The long-term goal, of course, is to find bijections where none are
currently known.  There is no shortage of open problems of this type, but
I would need to do some more homework to give a good list of examples.

Naturally it would be even better to automatically prove that the 
bijections are correct, but just finding and conjecturing seems hard
enough.

I should also mention a related, but in my opinion far more difficult,
project, which is to automate the process of finding combinatorial
*interpretations* of natural numbers that show up in various parts
of mathematics.  For example, often one obtains a vector space whose
dimension has some significance---it might be a Betti number, or the
dimension of some representation.  In surprisingly many cases, one
can get a lot of mileage out of finding a basis for the vector space
that is naturally indexed by some combinatorial objects.  Since vector
spaces in the abstract have no distinguished basis, finding such a
combinatorial basis requires some insight into the structure of the
variety or group or whatever that gave rise to the vector space in
the first place.  This seems to me to be out of reach of our current 
abilities to automate.  However, this problem need not be solved to
solve the easier problems I mentioned earlier.

Tim