[FOM] Re: Automated bijective proofs

[Jacques Carette]

"Timothy Y. Chow" <tchow at alum.mit.edu> wrote:
> On Tue, 29 Jun 2004, Jacques Carette wrote:
> > Indirectly however, there are two clearly relevant research threads:
> > Joyal's Theory of Species and the work of the ALGO project at INRIA
> > (http://algo.inria.fr).
> 
> Thanks for the information.  I know about species, but didn't know about
> the project to use that theory to automate combinatorics.  Such work would
> certainly be relevant to my question, although my first instinct is to 
> suspect that it's almost the inverse problem---i.e., finding algebraic 
> proofs of combinatorial facts, rather than finding combinatorial proofs
> of facts that are already known to be true by algebraic means.  

Actually, the goal of their project is to automate as much of combinatorics as possible, especially the analysis of 
asymptotic properties of combinatorial structures.  And the goal is to do this by any means necessary.  It has turned 
out that *analysis* (Mellin transforms, analysis of singularities, saddle-point methods, etc), and not algebra have 
been some of the most effective methods, although non-commutative Groebner bases in certain formal operator algebras 
have also had some remarkable successes in providing proofs for complicated multi-variate combinatorial identities.

This work is definitely not shallow - but may nevertheless not satisfy your needs.  As I said originally, this is an 
indirect research thread that may bear some light on your question.

Jacques