Proof Assistants being seriously useful for everyday garden variety serious mathematical developments

[Harvey Friedman]

Harvey Friedman wrote:
>
> OVERALL OPINION. The prospects for Proof Assistants being seriously
> useful for everyday garden variety serious mathematical developments
> look extremely remote for the foreseeable future. However, we all know
> something about some VERY SPECIAL SITUATIONS where there is a point in
> using them. In general, I like the investment in many of these. But
> THEY ARE UNUSUAL.

CABALLERO WROTE:

I am working precisely on this problem from the point of view that is
not mainstream. My approach is to develop the proof in the Wolfram
Language and then to compile it to a mainstream proof assistant, in my
case, to Isabelle/HOL, using the Isar language of human-readable
proofs. Reference to Isabelle/Isar:
https://mediatum.ub.tum.de/doc/601724/file.pdf
........

ME:

At what stage in the process a-e below would you think a serious
professional mathematician would want to use yours and any other
"proof software" to help when mired in state of the art details they
just barely understand themselves and where until normally final
stages, practically every statement is flawed?

a. Getting a Theorem proved in the sense of before any manuscript,
where the "proof" lies in mental images and scribbles on a piece of
paper or computer screen. Before any serious checking.
b. In the serious checking stage before writeup.
c. In the writeup stage constructing a first manuscript meant to
"verify" that it's all there for me only. Generally no one else would
get much out of it.
d. Perfecting the writeup so that it can be used to give a detailed
seminar presentation somewhat understandable to some experts other
than the author..
e. Perfecting the writeup further turning it into a real preprint
publicly available so advanced students can really get a good sense of
what is going on.

Just as a thought experiment. Where exactly in this process would
somebody being the original author proving the Invariance of Domain
(topology) or the Consistency of the Continuum Hypothesis or the
Existence of an RE set of Intermediate Degree, use yours or any other
proof management software?

Ordinarily important serious mathematical work is done by groping in
the dark, barely making any sense, then making some more sense, and by
the time it normally really makes sense and is somewhat close to a
flawed piece of real rigor, all of the normally interesting and
exciting creative work has been done, strictly from the practicing
mathematician's point of view, and getting to that point is the main
challenge.

That's why I say that it has to be some special situations where
software roughly of the kind you and others are talking about could be
useful out there in the real world. And of course important if one
wants real absolute rigor. I am interested in absolute rigor, both
theoretically and practically, but I distinguish it from the normal
serious mathematical adventures.

We all know about and value special situations - of course looking for
formal verification, normally after there is some real proof to be
verified. Or working out numerical and otherwise examples. Or graphing
data to look for conjectures. Or making calculations.

You could do the following. Go compile say ten major results proved
during 2020 in diverse areas of pure mathematics, and contact the
authors about their struggles to prove those results and what role if
any software would play for them.

It may be useful here to distinguish between proof software and other
special purpose software that we know is extremely useful.

Maybe you should consider focusing on targeting the special situations.

Harvey Friedman