[FOM] Automated bijective proofs

[Mitchell Harris]

On Sun, 27 Jun 2004, Timothy Y. Chow wrote:

>I wonder if there has been any effort to automate the process of finding 
>bijective proofs in combinatorics?
...
>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.

And a bijection in combinatorics is just a "simple" matter of finite set
theory? The difficulty I find with automating search for bijective proofs
(or combinatorial proofs in general) is that most are not very symbolic 

Combinatorial proofs are certainly rigorous, but just not amenable to
symbolic manipulation. In fact that is often the beauty of a bijection,
that it eschews blind algebraic symbol manipulation, and encourages
non-inductive intelligent manipulation of sets of objects. (I think this
rigorous but not formal proof style corresponds to Lakatos' term
"preformal"). And very intuitively, if there were to be invented a set of
inference rules for such combinatorial proofs, I'd expect the proofs to
rely on lots of uses of a cut rule (instantiation of intermediate
identities) that would increase the search space/time considerably.


>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 don't think this was your point, but if one interpreted all the
machinations of the WZ method appropriately i.e. combinatorially), one
could extract a combinatorial bijective proof. I don't think the 
combinatorial proof would say anything new, but possibly the 
combinatorial interpretation of the general WZ process (or any other 
similar proof system) might be new. 

The species/combinatorial-PDE correspondence gives proofs of equality
after the PDE is created. The creation of the PDE formula or species
constructor is the main intellectual work of a combinatorial proof, for
which I have not seen any attempts at a systematic proof method.

On the other hand, once a few algebraic/combinatorial tricks are learned
(addition <-> disjoint union, multiplication <-> ordered pair (or
sequence), binomial <-> some subset, (-1)^k <-> inclusion/exclusion,
etc.), many hints for a proof can be extracted from an algebraic
statement, which is good for humans but who knows for an algorithm.

-- 
Mitch Harris
Lehrstuhl fuer Automatentheorie, Fakultaet Informatik
Technische Universitaet Dresden, Deutschland
http://lat.inf.tu-dresden.de/~harris