I like to present a conundrum facing this fine ambition as follows (see my "computist quiz" on the fun www.hackersdelight.org for more) ======== Define a predicate on positive integers (in Javaesque style): boolean isToad(int n) { return n==2 || n==frog(4,floor((n-1)/2),1,0)-1); } with the aid of the following helper method: int frog(int q, int r, int s, int t) { if (r<t) { return 0; } else if (r==t) { return 1; } else if (q==0) { return 0; } else { return frog(q,r,s+1,s+t) + frog(q-1,r-t,1,0); } } ======== Now we pose three queries, in increasing order of difficulty: 1. Which integers are toads? 2. Describe what the frog method does. 3. Can you explain why this code works? With these denouements: #1: Running the program, one quickly sees that the Toads are the primes. #2: After lots of tedious tracing, most programmers painfully realize the code is *not* doing some kind of division-by-subtraction. (What it *is* doing I'll leave as a puzzle for those inclined). #3: The explanation is essentially a fairly non-trivial theorem of Legendre. Automatically finding such a justification for the bald assertion "the predicate is true just if N is prime" seems implausible anytime soon. Worse, this may not even be asserted explicitly, but implicitly required as a lemma (such as if the predicate is called as a subroutine within larger programs). While the above example seems like a big jump to us, if we imagine a future of increasingly harder proofs, it would eventually become the norm, then a triviality. But this is really no different than zillions of other facts humans depend on unconsciously in verifying correctness. For example, we depend on knowing, without reproof, that if we add 1 to a variable it will get larger, that if we add an even number its oddness will be conserved, and so on. Admittedly artificial, but this illustrates just how wide the gap could be that we may implicitly be asking a mechanism to fill, and how much is gained in human proofs by ready reference to "known" results--not just from citing them, but by being able to select the relevant ones and apply them aptly. ======== But, having said all that, I still think that there's something valuable in Henry Baker's suggestion. Surely leveraging our growing automation resources would be a good thing. I think the trick to making it successful will be to find a way to plug each piece into an ever-growing machinable context, (much as the web itself grows) rather than imagining each case in isolation, stranding some forlorn AI on a hard proof's desert island, provisioned with nothing more than some axioms and rules of inference.