[FOM] SHIFTING PARADIGMS?

[Timothy Y. Chow]

On Tue, 29 Jul 2014, Josef Urban wrote:
> There is some seminal work on general conjecture making in number theory 
> (Lenat - AM) and perhaps graph theory (Fajtlowicz - Graffiti), but I 
> don't think we have shown how to do this for most of math. And even if 
> the conjecture-generating part was not so hard, we are nowhere near 
> finding proofs of new interesting conjectures in most of math 
> automatically

One area where I think it would be very interesting to advance the state 
of the art in automated theorem proving is bijective combinatorics.  It is 
traditional in combinatorics to regard bijective proofs of identities as 
providing great mathematical insight, and sometimes to require great 
mathematical ingenuity.  However, I don't see any reason in principle why 
computers could not be programmed to search for, and prove the correctness 
of, bijections.  It's not a trivial project by any means but I think it 
could pay enormous dividends.  As a first step, one could try to program 
computers to rediscover some known celebrated bijections.

Tim