[FOM] Talk on Formal Verification

[Lawrence Paulson]

My point is that this example can be answered immediately with the statement "prime numbers don’t behave like that" with no effort, or more rigorously by recollecting the prime number theorem, with a miniscule effort. There is no need to think up a concrete solution unless one is demanded. Tim Gowers has a second example: to consider the series of numbers 41, 43, 47, 53, 61 (where the difference increases by 2 each time) and ask whether all the numbers in this series are prime. The intuitive answer is once again "prime numbers don’t behave like that”. The rigorous answer is to note that these integers are generated by the polynomial n^2 + n + 41 and to consider n=41.

I'm not aware of any software that can begin to get to grips with any problem involving a bit of intuition and a bit of domain=specific knowledge. An expert system on elementary number theory could be created, but we would be able to step outside of its area of expertise very easily.

Larry Paulson


> On 4 Feb 2016, at 00:52, 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?