879: Structural Proof Theory/11

[Michael Lee Finney]

> By JUMPS I mean the JUMPS that proof assistants will definitely have
> to make if they are to realize the MOST AMBITIOUS GOALS. And JUMPS
> they will definitely have to make in order to get more and more
> powerful on the MORE REALISTIC GOALS. We should be generating lots of
> toy problems with huge mathematical challenges to meet. My general
> methodology is to GO INTO THE PURE SITUATIONS where one SEVERELY
> LIMITS what the TECH is given, and see what it can realistically find.
> AND HOW IT DOES FIND. That way, JUMPS are seriously confronted. AND
> because of the superclean pared down structure of these setups, THE
> PROSPECTS FOR IMPORTANT FRUITFUL TOY PROBLEMS with tremendously
> interesting THEORETICAL CHALLENGES, is maximized. NOT SO in situations
> where the TECH is given everything with the kitchen sink.

> Harvey Friedman

The problem is that JUMPS, both minor and major, essentially require general
artificial intelligence -- and we have no clue on even how to start with that.
People have been working on that for a number of decades and exactly zero
progress has been made. If you look at textbooks from 25 years ago, about the
only difference between then and now is a bit of tweaking. And using very large
datasets with very large computers. There is a lot of noise about beating
chess or go master players, self driving cars, language translation, etc. All
of those are great and are wonderful achievements -- but at their heart, they
are just really, really large statistical models using enormous amounts of
data and processing power. Some of it is accomplished by searching huge spaces
with extremely large and powerful computers, combined with a large set of
rules to prune the space. And a large dataset of existing positions with known
solutions.

But, none of that helps with JUMPS. It may help with proof understanding, but
the essence of the technology requires huge amounts of data (think terabytes
or even petabytes -- gigabytes is just a toy student problem). And we probably
don't have enough data to really do a good job there. Understanding proofs is
not the same as natural language understanding, it has its own style and much
of that is understanding what is omitted as much as what is present. Since
many publications are by those who are non-native language speakers, even the
grammar is likely to be an issue.

We are a long, long way from the point that we can handle JUMPS, large or
small. What we can handle is verification and assistants -- especially for
simpler areas such as pure logic. A certain amount of theorem proving can also
be done. But, it requires careful formalization and specification. It isn't
just a matter of stating a theorem and telling the software to "prove it". I
am not acquainted with the current batch of theorem provers, but my
understanding is that most or all of them rely on techniques which
intrinsically assume the law of excluded middle and / or contraposition. That
means that they don't work well in areas without those or where constructive
proofs are desired. I don't see them developing a proof plan from a high
level, and then filling in the blanks. That requires a human level of
understanding of the subject domain.

What might work to some degree is more of a rule based approach combined with
state space searching. That also requires a large database, and almost
certainly custom to a specific area of mathematics. That database would be
similar to the rules of thumb that graduate students learn. That might help in
bridging the gaps and in proof understanding. That might make proof assistants
and verifiers more likely to be able to work with conventional proofs without
the effort required to translate the proof or problem as much as is needed
now.

But, really, the technology is probably many decades away from handling JUMPS
of any nature. JUMPS are what require human level intelligence, and there is
no technology today or on the horizon enabling that. We are all hoping for a
breakthrough any day now, but we have been hoping for that for decades and are
still disappointed.

All of that said, I believe that technology can be of great assistance in
working with most areas of mathematics. Each problem might require custom
software, but that is no different than using technology in other areas.

Michael Lee Finney