[FOM] Talk on Formal Verification

[Timothy Y. Chow]

Lawrence Paulson wrote:
> Here's a different example, due to Tim Gowers: does there exist a series 
> of 100 consecutive composite numbers? (Of course there does, by the 
> prime number theorem. But what about a constructive proof?) I don't 
> think that a computer has a hope with this type of problem. For all its 
> achievements, AI has accomplished nothing that resembles insight or 
> creativity.

I agree that AI has not yet achieved insight and creativity in the sense 
that you intend here, but I don't understand your example.

Yes, of course there exists a sequence of 100 consecutive composite 
numbers:  101! + 2, 101! + 3, 101! + 4, ..., 101! + 101.  (Using the prime 
number theorem seems like a perversely complicated proof.)  What is it 
about this example that is supposed to be particularly hard for AI?

Tim