[FOM] formal proofs

[Josef Urban]

On Thu, Oct 16, 2014 at 4:55 AM, Harvey Friedman <hmflogic at gmail.com> wrote:
> On Tue, Oct 14, 2014 at 10:54 AM, Josef Urban <josef.urban at gmail.com> wrote:
> ...
>> Voevodski describes in
>> http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf
>> several situations of recent buggy proofs and contradictory theorems
>> in his field that stayed unresolved for some time, and how he started
>> to feel uncertain about possible errors produced in "high-level" math
>> research.
>
> It would be informative to get a sense of what the community engaged
> in this "high-level" math has to say about "recent buggy proofs and
> contradictory theorems"

Yes, although to me it is already informative when a Fields medalist
talks this way about his field(s).

To get some "objective sense" of what the wider community thinks, one
could try sentiment analysis [1] (the crudest is grepping for "error"
and its synonyms) on a large body of mathematical papers (arxiv,
Google Scholar). That could give an "error scale" of various fields.

[1] http://en.wikipedia.org/wiki/Sentiment_analysis#Methods_and_features

A simple experiment (by a complete outsider): Bloch's 1986 paper
mentioned by Voevodsky has 501 Google Scholar citations [2], and
searching within them for "error" quickly yields a 1990 paper by Bloch
in which he acknowledges the error and claims to have "another proof,
but it is too complicated to inspire confidence at this point,..." .

[2] http://scholar.google.com/scholar?cites=14786540277760456849&as_sdt=2005&sciodt=0,5

> and their take on the usefulness of ideas
> being proposed for "fixing" or "improving" the situation.

I have no idea. Neither about what that community thinks, nor about
the usefulness of (homotopy) type theory (HoTT) as (new) foundations.
I think that computer-understandable math is our inevitable future,
but the main issues to solve are good automation and human-computer
understanding mechanisms (the two are related), not so much yet
another foundations. Sometimes foundational proposals in formal math
are actually automation proposals.

> Also to get
> an idea about how high the "high-level" math is that you are referring
> to. Here are some obvious naive questions:
>
> 1. What parts and what subparts of math have "recent buggy proofs and
> contradictory theorems"? I found this on Math Overllow
> http://mathoverflow.net/questions/5485/how-many-mathematicians-are-there
>
> "Current count of Mathematics Genealogy Project is 137672 (I am
> assuming that the PhD students that graduated are ranked as "research
> mathematicians"). But the problem is.. Mathematics Genealogy is mostly
> for universities of developed countries. There could be some really
> good university in Russia, China or Korea out there that doesn't give
> us the correct statistics. Another problem is.. Mathematics Genealogy
> Project counts even the dead mathematicians (like Hilbert, Hasse,
> Kepler and so on).. and I am assuming you want a report of living
> mathematicians.. but hey, I'm quite surprised by the number even 200k
> is pretty low for the living!"

Another motivation for the kind of analysis suggested above?

>
> 2. What is the absolutely simplest watered down specific situation
> that you can explain to anybody where one can get even a glimpse of
> advantages in doing something differently than the usual? I.e., get
> down to the essence of the issues being addressed. If you can present
> this, then people like me can probably construct many alternatives for
> handling it, some of which may be worthwhile - as well as new
> metatheorems and transfer principles. THese are in the arena of
> "special purpose tools" to address the issues. Such work simply cannot
> be done by people who are not trained and steeped in f.o.m. - even if
> they have good credentials.

This seems to be a question addressed at proponents of HoTT (I am not
one of them). In fact, I would like to hear some clear answers to this
myself. What I heard so far either did not convince me as general
foundational claims, or it assumed so much type-theoretical background
that I did not understand.

>
> 3. As I invariably indicate on the FOM, it is greatly preferable to
> have honest accounts that are completely accessible and transparent,
> in an interactive setting. Even if some people think they are
> repeating themselves.
>
> 4. It would also be interesting to hear what you and others have to
> say about the wide ranging issues raised in
> http://www.cs.nyu.edu/pipermail/fom/2014-October/018214.html

Hales talks about many of these issues in Sections 2 and 3 of
http://arxiv.org/abs/1302.2898 .

I'll add one comment about the "Holy Undecidability". The same Turing
who proved undecidability in 1936, has built the first computers,
wrote the first chess program, and his 1950 paper on Computing
Machinery and Intelligence has started AI. There he says that "We may
hope that machines will eventually compete with men in all purely
intellectual fields" and proposes chess as one of the fields where one
could start teaching intelligence to machines. I believe he would be
happy with the prospect of having large corpora of
computer-understandable math for this task.

In other words, I don't believe that manually crafted "little engines
of proof" are the best we can do. Undecidability says nothing about
our ability to build strong AI that will do general math on a level
that is comparable to the best mathematicians.

Josef