Timothy Y. Chow tchow at alum.mit.edu
Tue Jul 29 22:17:12 EDT 2014

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.


More information about the FOM mailing list