Clarification of Skepticism

[Harvey Friedman]

I think I need to clarify my Skepticism.

Serious mathematics generally involves major intellectual JUMPS. I see
no evidence that these JUMPS can be simulated by any proof
technologies.

At the core there are normally major intellectual jumps that do not
seem to fit into possibilities in manageable sized spaces, or are
amenable to reinforcement techniques and so forth.

HOWEVER, I do believe that serious mathematics also involves keeping
things straight, and also MINOR intellectual JUMPS. But bookkeeping
and minor intellectual jumps can be the sorts of things that are
amenable to technology. I understand that several FOM writers like to
use technology for minor intellectual jumps and management. But the
incentive to do so without the prospect of it coming close to
affecting Major Intellectual Jumps, doesn't seem to be there - unless
you are already invested in some ways.

My work usually involves several major intellectual jumps, more minor
intellectual jumps, and a fair amount of management. Whereas I can
imagine some use of technology for the minor intellectual jumps, and
the management, I do not imagine that for the several major
intellectual jumps. And many of those major intellectual jumps, aside
from POWERFUL MATHEMATICAL IMAGERY AND CREATIVE IMAGINATION, involve
PHILOSOPHICAL REFLECTION, EXPERIENCED JUDGMENT CALLS, and DISCOVERIES
OF NEW KINDS OF MATHEMATICAL STATEMENTS RESULTING FROM DECADES OF
CONSTANT REFINEMENTS AND EXPERIMENTATION.

The minor intellectual jumps and the management, are so trivial in
comparison, that I barely even notice them.

Now some of my projects - mostly unfinished - explicitly involve the
analysis of a large but feasible set of finite structures. Obviously,
technology can be crucial in such a context because the objects can be
systematically explored by the technology in ways that are not
feasible by the human brain. As a notable example, my proposals for
the use of technology to search certain finite spaces which confirm
the consistency of large cardinal hypotheses. But this is a
specialized and unusual use of technology and not really proof
assistants.

As you can see from earlier postings, I got interested in where the
intellectual JUMPS become inaccessible to proof assistants. So I went
into toy situations where the challenges are in a comparatively pure
form. To take a ridiculously extreme case, look at the JUMP needed to
go from ZFC to FLT. Is there anybody here on FOM that thinks that by
2100 one will be able to make that JUMP, from ZFC with exp to a proof
of FLT in ZFC?

I would like to see an understandable discussion, without JARGON, of
what kind of JUMPS can already be made or are in the cards to be made
by proof technology.

Harvey Friedman