Can Proof Technology Even Do this?

[Harvey Friedman]

In my quest to tone down some wild enthusiasm and accusations that I
don't smell the flowers, this get serious about the issues proof
technology faces BEYOND WHAT WE HAVE KNOWN FOR DECADES ARE ITS
STRENGTHS.

I want to be fair to the poor burdened challenged proof technologies.
WIth regard to the huge success with chess and alphazero, and also I
gather the recognize breeds of animals through pictures, etcetera, and
also go, of course, I assume there has evolved some

        normal form for presentation of the problem

Roughly speaking, alphazero is supposed to have been given the "rules
of chess" and told to get to work. So I assume a well worked out
normal form of presentation for such a challenge is either kind of
obvious or has been worked out well.

Similarly, we could develop perhaps MORE THAN ONE, standard normal
form of presentation for proof technologies to be given

a formal system S and a sentence phi, and the problem is to prove phi from S

The obvious setup of course is a decent dialect of predicate calculus
with axioms and rules of inference and a sentence phi, where the axiom
system is presented with finitely many axioms and finitely many axiom
schemes.

So let us do START FROM SCRATCH. The reason it is interesting to start
from scratch is that everybody knows exactly what is the starting
point. Of course the endpoint phi is not going to be anything close to
anything close to any state of the art. Instead I AM CONCERNED WITH
how easy phi can be so that proof technology can do it, or WHAT KIND
OF HOPE DOES PROOF TECHNOLOGY have of ever doing it, and everything IN
BETWEEN. THEN the idea is to scale upwards, so that if we have a big
KNOWLEDGE  BASE and TECHNIQUE BASE, we have at least some idea of WHAT
KINDS OF MATHEMATICAL JUMPS are realistic. IT"S REALLY THE JUMPS that
proof technology does, can, or will make, that we want to understand.

**OBVIOUS POINT NEED MAKING** The following two things MUST BE DISTINGUISEHD.

1. Is there a feasible size piece of software that will do things like
find proofs of FLT and RH from ZFC scratch, say one that fits into
your state of the art memory on your computer running on your desktop?
2. Is there a feasible size piece of software that will do things like
find proofs of FLT and RH from ZFC scratch, say one that fits into
your state of the art memory on your computer running on your desktop,
WHICH HUMAN BEINGS ARE CAPABLE OF CREATING?

At the extreme 1 is if in fact all these problems are doable in ZFC.
For just compile their proofs and the software simply copies it out
when asked. And I can imagine more sophisticated possible answers to 1
being possible as the STATE OF AFFAIRS. However, 2 is an ENTIRELY
DIFFERENT MATTER. And so when discussing what proof technology can and
will do, let us remember that humans are creating this proof
technology for the purposes of this discussion.

END OF DIGRESSION.

Now for some down to earth CHALLENGES. Ranging from controversially
hard to absurdly hard. (No Libraries hee but see my comments about it
is the JUMPS that we want to understand and evaluate).

A. Start with the axioms of Peano Arithmetic in the language of
0,S,+,x, the usual with finitely many axioms and the induction scheme.
Prove: every number is of the form n+n or n+n+1 but not both.
B. Same start as A. Prove: commutative, associate laws for +,x, and
the distributive law, and also the monotonicities.

Now here with A,B we expect a lot of successes, but since we are soon
going to have nothing but FAILURES, I suggest we dwell on the inner
details of the successes with A,B. For example. DO WE GIVE THE TECH
THE HINT THAT IT IS GOOD TO TRY INDUCTIONS OUT FOR FORMULAS THAT ARE
VERY CLOSE TO WHAT IS BEING PROVED? This immediately suggests various
notions of SELF PROVING in arithmetic. And some expected difficult but
INTERESTING problems about when things stay SELF PROVING in this
sense, and when they PROVABLY GO to the NON SELF PROVING. I.e., new
kinds of practical proof theory of arithmetic. One could for some of
these explorations, go to PRESBURGER.

In other words, look for Theorems to the effect that

SUCH AND SUCH STATEMENTS IN ARITHMETIC ARE SELF PROVING
SUCH AND SUCH STATEMENT IN ARITHMETIC ARE NOT SELF PROVING

C. Start as in A and prove n x n not= 2.

I don't know how to state this but I believe in it: n x n not= 2 IS
NOT SELF PROVING IN PA. And this should be established in PA with
primitive recursive FUNCTION symbols.

AS FAR AS I KNOW, you pretty much need to define F(n) = number of
times 2 divides into n, and then prove F(n x n) = F(n) + F(n). So to
be fair to the proof technology, ALLOW PRIMITIVE RECURSIVE FUNCTION
SYMBOLS. But our tech needs to come up with the right function symbol.
One simple approach is not directly such a nice primitive recursion:
F(2) = 1, and for all n >= 2, F(n x n) = F(n) + 1, Or more generally,
base it on F(n x m) = F(n) + F(m). F(2) = 1.

BUT should we tell the technology to use one of these functions with
those equations? Of course, then things get comparatively trivial. BUT
HOW DOES THE TECH come up with the idea of "number of times you can
divide 2 into a number" and then execute it properly?

D. Same start, but prove if a prime divides a product then it divides
one of the factors. Then move on to for all n there exists m > n such
that m is prime.

E. Same start, but prove for all n there exists m > n such that m and
m+2 are prime.

WHAT GIVES ME PAUSE ABOUT SOME OF THE THINGS OPTIMISTS SAY ABOUT PROOF
TECHNOLOGY is that the jumps that a serious state of the art
mathematician routinely makes from the existing knowledge for a
serious result is VERY VERY LARGE by many standards.

But if we can spot those UNUSUAL CASES where the jumps are of a
SPECIAL CHARACTER, then the tech can be useful.

Of course, OBTAINING ABSOLUTE RIGOR, WORKING OUT EXAMPLES, VISUALIZING
STUFF ON THE SCREEN, etcetera - sure we are doing this all the time.
Even MAKING CONJECTURES IN CERTAIN CONTEXTS yes, too.

Harvey Friedman