Technology for Which Mathematical Activities?/1

[Josef Urban]

Some quick comments on the AI/TP topics.

1. There is an ongoing seminar on these topics with recordings on YouTube
organized by Mike Douglas: https://cmsa.fas.harvard.edu/tech-in-math/ .
This Wednesday there will be a talk by Jason Rute about a recent AI/TP
system for Lean. There are also many talks recorded from AITP'20 at
http://aitp-conference.org/2020/ .

2. Conjecturing has been getting more and more attention. Several
statistical/ML/TP methods have been proposed in the last five years (see a
short overview in https://arxiv.org/pdf/2005.14664.pdf). It is still a very
hard task and the methods are still pretty basic, but e.g. the recent
neural architectures can sometimes produce quite good-looking conjectures
and even full proofs. It starts to be fun.

3. This is related to autoformalization (automated translation of TeX to
formal math), which also seems to be a more and more realistic task. Again,
thanks to combinations of (better) learning systems and theorem proving
methods.

4. The raw power of standard ATP systems is still quite low in general
math, but it has improved quite a bit over the last couple of years. We
went from about 40% on full Mizar in the last big evaluation in 2014 (
https://doi.org/10.1007/s10817-015-9330-8) to almost 60% today in a
comparable (resource controlled) scenario. You can take a look at examples
of what we can prove automatically (typically under 60 seconds CPU time)
here:  https://github.com/ai4reason/ATP_Proofs .

5. In tactical ITPs (HOL, Coq, ...), the situation may be even better. The
TacticToe system (https://arxiv.org/abs/1804.00596) by Thibault Gauthier
has proved about 70% of HOL4 theorems in 60 CPU seconds already in 2018.
Again, this is thanks to guiding the tactics by learning from previous
proofs. Similar systems now exist also for HOL Light, Coq and Lean.

Thanks to (4) and (5), I have basically already won the second part of my
bet (2) from my 2014 challenges (http://ai4reason.org/aichallenges.html).

I am still happy to accept bets on the other challenges from the naysayers
;-).

Best,
Josef


On Sun, Feb 28, 2021 at 6:08 PM Harvey Friedman <hmflogic at gmail.com> wrote:

> The various postings expressing optimism about the use of technology
> based on current developments have NOTHING TO DO with what I am
> saying.
>
> For various specialized tasks of interest, there has obviously been
> more and more useful technology.
>
> For certain other tasks of even greater interest, progress appears
> totally unthinkable at the moment.
>
> I really was only making my obvious point IN PASSING. I was setting
> the stage for discussing what are the REALISTIC outcomes of proof
> technology research that have been OVERLOOKED and that I do think are
> FEASIBLE, although difficult.
>
> I will by the way defend attacks against me for finding TEX a
> disgusting nuisance. But I don't think that this is a useful
> discussion for FOM.
>
> As far as technology is concerned, music performance software of the
> kind I had to master some of (say DP), makes Tex look like a
> specialized joke, and is REALLY useful. I created a new kind of piano
> recording based on thousands of hours of micro editing with this
> splendid technology which makes tex output look like a minor ugly
> eyesore in comparison. If you are interested in this path breaking
> story in piano performance you can talk to me offline. I credit my use
> of this performance software to my being well on the road to top
> professional classical pianism in the ordinary sense with fingers. I
> would be interested if the use of TEX can be credited for putting
> people well on the road to top professional mathematics.
>
> WE ALL KNOW THAT technology help for doing mathematics is around. The
> real question is: for what kinds of things? Making completely
> unsupportable claims of prospects that are totally unwarranted,
> instead of FOCUSING ON the kinds of things that are realistic, is
> rather counterproductive with the general mathematical community.
>
> I suggest we compile and discuss a list of things, generally
> explainable, which have yielded progress and we can expect more
> progress. And say something new maybe about this. Here are some.
>
> 1. HELP IN formulating conjectures. NOW this is only realistic in
> CERTAIN KINDS OF MATHEMATICS. Interesting to understand which kind it
> is and which kind it is not. If it involves VISUALIZATION, hen of
> course. Generating pictures on a screen can be a huge addition to
> generating pictures in the mind or on paper. Would be interesting. And
> obviously certain kinds of discrete mathematics, involving counting
> finite sets, particularly when the challenges already surface in the
> manageable finite, is another.
>
> 2. HOWEVER: help in formulating conceptual breakthrough conjectures is
> another matter. Finding the right conjecture that explains some
> mysterious phenomena, or yields a startling revelation about a field -
> thee are crucially important endeavors. For instance, Goedel came up
> with the precise statement that is now known as the COMPLETENESS
> THEOREM FOR PREDICATE CALCULUS. Then proved it. Would he benefit from
> technology to even think of the completeness theorem?
>
> 3. AND HOWEVER, help in formulating KEY DEFINITIONS. Frege invented
> first order predicate calculus. Are we going to say that with the help
> of computer technology, this would be facilitated?
>
> 4. Also tell me how computer technology is going to help Solovay and
> Reinhardt lay out the fundamental large cardinal hierarchy based on
> nontrivial elementary embeddings? And tell me how computer technology
> is going to help Cohen discover forcing, or Goedel discover L?
>
> 5. ESTABLISHING ABSOLUTE RIGOR. That, like 1, is where the technology
> has really made a difference. BUT doing this for a big theorem BEFORE
> it has really been well understood? Like - I have a pretty good idea
> of how to prove the Riemann Hypothesis maybe in about 50 pages using
> this and that this way and that way. Before I really can understand
> the details of how the subtle parts work together, I will use my proof
> assistant. I AM VERY DOUBTFUL ABOUT THIS. After the big theorem has
> been fleshed out and well understood, THEN with the technology doing
> proof verification IS GENERALLY VIABLE, although it is still
> INCREDIBLY TIME CONSUMING. WHAT ABOUT formally verifying FLT? I have
> no doubt that this will be done by 2100, but WILL INVOLVE SERIOUS
> REWORKING AND SIMPLIFICATIONS of the proof and a lot of serious time
> commitments. And the key ideas in those preliminaries are just not
> going to be using technology.
>
> 6. FINDING ERRORS. There are, as I understand it, some interesting
> cases of this. I would like to HEAR MORE ABOUT THIS. Obviously very
> unusual, but very interesting. ESPECIALLY if we can use this to help
> us see SYMPTOMS OF where conventional acceptance of theorems can go
> wrong.
>
> 7. NOW LET'S GET REAL. Instead of my making all this fun about this,
> WHERE ARE THE UNUSUAL situations? What are they like?
>
> I still haven't got to my main points about WHAT FOUNDATIONAL
> INFORMATION CAN BE HOPE TO GET OUT OF THE TECHNOLOGY? I.e., Structural
> Proof Theory.
>
> Harvey Friedman
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210301/4ea1c0ff/attachment-0001.html>