[FOM] formal proofs

[Harvey Friedman]

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" and their take on the usefulness of ideas
being proposed for "fixing" or "improving" the situation. 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!"

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.

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

Harvey Friedman