[FOM] Talk on Formal Verification

[Mario Carneiro]

On Wed, Feb 3, 2016 at 7:52 PM, Timothy Y. Chow <tchow at alum.mit.edu> 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?
>


I think Lawrence's point is, how hard would it be for a computer to
recognize that 101! is the key number it needs for this construction?
Without some guidance it is likely to try brute-forcing, and it will take a
long time to get to 101!, if indeed it gets there at all. Sure, as
mathematicians we can "trivially" come up with the answer, but the point is
that computers are not as good at making these kind of intuitive leaps.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160204/3c1fdbab/attachment.html>