[FOM] Talk on Formal Verification
hendrik at topoi.pooq.com
Thu Feb 4 05:29:50 EST 2016
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.
More information about the FOM