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

Thu Feb 25 02:14:40 EST 2021

Dear Prof. H. Friedman
  I quickly answer your questions and comments.

Question 1:

> 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 user-friendly proof assistant brings mathematical rigour to those
deprived of access to a rigorous expert in a particular field to check
their work. Also, there is a brilliant mathematician that is extremely
creative but not rigorous in their proofs. In these cases, a proof
assistant is like a textbook that can be used anytime during the research
process.

In my particular, that is not mainstream, a proof assistant developed
inside a powerful symbolic algebra system (Wolfram Language), having an
interface of natural language (Wolfram Alpha) and developed
graph-theoretical tools, is not just a way to check what was done on paper,
but also a tool for exploration far superior to the original symbolic
algebra system in which it is developed. The (heuristic) reason is the
principle of computational irreducibility: exploration is a fundamental
part of mathematics that cannot be avoided regardless of the
mathematician's skill. A computer can explore the computational universe of
a given mathematical theory faster than a human. Indeed, it was written in
A New Kind of Science:

as soon as one look at cellular automata or other kinds of system beyond
> those normally studied in mathematics it must immediately become
> effectively impossible to make progress using traditional mathematical
> methods.

https://www.wolframscience.com/nks/p793--implications-for-mathematics-and-its-foundations/

Question 2:

> 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?

In the case of mainstream proof assistants, the author (mathematician) of
the Continuum Hypothesis's Consistency will not use the proof assistant. It
will be formalized by a computer science researcher/student and submitted
to the Archive of Formal Proofs.

In the case of my proof assistant, if the author knows the proof, he can
use my proof assistant to check it or ask another person to do it for him.
If the author knows the theorem but does not know the proof, then he can
use my proof assistant to explore the computational universe related to the
theorem. As with any exploration, the mathematician's responsibility is to
use his intellect to find patterns (the computer may help to some extent
since it detects patterns). Finally, if the mathematician only has a formal
system and wants to explore it, a proof assistant integrated into a
symbolic algebra system may be the only viable day to do it. Here is an
example of such an exploration of a set of axioms:

https://www.wolframscience.com/nks/p773--implications-for-mathematics-and-its-foundations/

The role of the compilation from my proof assistant to Isabelle/HOL, and
maybe shortly the other way around, is to take the best of both
technologies: the Wolfram Language (computational algebra and graph
theory), Wolfram Alpha (natural language processing) and Isabelle/HOL (type
theory).

Comment 1:

> 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.

Some mathematicians, like Archimedes, Euler and Gauss, were masters of
empirical explorations. They made a lot of trial and error before finding
the elegant statements and proofs that immortalized their names.

Comment 2:

> 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.

I do not know according to whom I should consider these ten results. So, I
will talk about my work published in 2020. The computational exploration
was crucial to see a new and beautiful theorem connecting theta functions,
the distribution of divisors of an integer and context-free grammars. I
transformed sets of numbers into context-free languages, and I derived
properties of the sets from the languages' properties. There are many
mathematicians involved in my paper's subject: Kronecker, Jordan, Erdos,
Tao. Still, the method of proof was strongly suggested by its empirical
derivation using the software.

http://math.colgate.edu/~integers/u2/u2.pdf

Comment 3:

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

I agree that proof software has a bad reputation, at least in the
mathematical community, whereas other software, like symbolic algebra
software, has a good reputation. Nevertheless, I hope that this is because
of contingent historical reasons and not because of something intrinsic to
the task's nature. Indeed, in my approach, proof software is developed
inside algebra software, dissolving the problem's boundaries.

Concerning proof assistants, I do not see any mathematical obstacle for
their applications. It looks to me instead as a problem of engineering.

Kind regards,
José M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210225/23428dc8/attachment-0001.html>