[FOM] Talk on Formal Verification

[Hendrik Boom]

On Wed, Feb 03, 2016 at 07:52:42PM -0500, Timothy Y. Chow wrote:
> 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?

Presumably thinking up the idea of 100!  That requires some insight.

-- hendrik