Clarification of Skepticism

[Lawrence Paulson]

> On 2 Mar 2021, at 01:56, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> Serious mathematics generally involves major intellectual JUMPS. I see
> no evidence that these JUMPS can be simulated by any proof
> technologies.

You are right here, and most people working in the field would agree with you. Most of us are trying to assist mathematicians rather than to replace them. What you should hope for in the foreseeable future is reliable assistance in checking those things that you regard as obviously true, but aren’t always. Automatic counterexample checking is already useful in some problem areas.

There are plenty of examples that involve an intellectual leap, and not even a major one. The mutilated chessboard is a well-known and particularly simple example. Interestingly enough, modern technology has progressed to the point where the original version for an 8 x 8 chessboard can be solved by brute force alone, without the use of any insights, but this isn’t what we want. Brute force can easily be defeated by making the chessboard bigger.

Larry Paulson