Clarification of Skepticism

[Josef Urban]

I am willing to bet that

1. FLT will be formally verified by 2050.

It seems quite conservative given the recent progress. If things go well
and formalization gets easier and ubiquitous, it could happen quite a bit
faster.

Then there are:

2. A computer suggests FLT.

3. A computer suggests Tanyama-Shimura.

4. A computer proves automatically FLT.

None of them are as easy to precisely state as (1).

They depend on what the machine is allowed to know beforehand.

(2) seems similar to what has been done by Lenat, Langley and Colton
decades ago. And it looks really short (could be generated just by
enumeration).

(3) really depends on what the machine is given. Holmstrom & Vik have been
playing in related areas recently:
https://link.springer.com/chapter/10.1007/978-3-319-62075-6_13 .

(4) could be stated as "having just as much ZFC and its number theory
needed to formulate and prove FLT". And then the machine would have to
discover and prove everything along the way to FLT. This sounds relatively
clean, but also much harder than what Wiles did - he knew a lot already. It
would be a serious jump.

Still, my estimate is that by 2070 (4) will be done in some way. Because
machines will get much better in proving and in proposing interesting
concepts and theories, including smaller and bigger jumps.

In particular, the things listed below don't look impossible:

- "imagery": has been demonstrated in various ways mentioned before. This
may need to be lifted from low-level/syntactic to more higher-level/fuzzy,
but such methods are coming and experimented with.

- "philosophical reflection": not sure if/how it will be particularly
needed beyond judging interestingness of math concepts and theories.
Perhaps grounding in real physical world will turn out more important for
developing the kind of math humans have focused on.

- "judgement calls": AlphaGo/Zero have learned them better than humans. Its
setting is much more limited than math, but you can clearly see the
algorithmic progress ("jumps") from zero knowledge to superhuman.

- "decades of refinements/experiments":  AlphaGo/Zero has self-played more
games in days than any human has played in his life. It wouldn't be too
hard to have it play more games than all of humanity ever played.

All of this is certainly much more speculative/pointless/hype-ish than my
cautious/precise "40/60/80% of Mizar/Flyspeck/AFP/etc". So I prefer to
focus on the latter as the real goals where we can measure day-to-day
progress.

But I don't think the underlying arguments differ much from what Turing was
saying already in his 1950 paper when addressing various objections to AI.

Best,
Josef



On Wed, Mar 3, 2021, 05:36 Harvey Friedman <hmflogic at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210303/1e13cd7e/attachment-0001.html>