# [FOM] Talk on Formal Verification

Colin McLarty colin.mclarty at case.edu
Thu Feb 4 14:56:21 EST 2016

```I really doubt that Tim Gowers thought AI would never be able to think of
factorials in the search for runs of composite numbers.  What could be more
paradigmatic of composite numbers than factorials, or a more convenient
source of numbers with many factors?

Much more likely he was thinking of the sort of results he has been
getting lately, and much prominent work by others, on the distribution of
prime gaps.

Colin

On Thu, Feb 4, 2016 at 7:37 AM, Mario Carneiro <di.gama at gmail.com> wrote:

>
>
> 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
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160204/49e2bfe0/attachment.html>
```

More information about the FOM mailing list