Questions on proof assistants

[José Manuel Rodríguez Caballero]

JS wrote, concerning proof assistants:

> My questions are:
> 1) which of these can make use of work done in which other ones?
> 2) which of these would be the easiest for mathematicians with some
> programming experience to learn to use to create machine-verifiable proofs?
> 3) which of these have a good translator that turns a machine-readable
> proof into something a human reader might gain insight from?


I will write from the perspective of my personal experience, for other
people it may be different. So, I will not address question 1), which is
more for experts in computer science. My background is pure mathematics
(number theory) rather than computer science. So, I belong to case 2),
i.e., I learned Isabelle/HOL when I was finishing my Master's degree in
Mathematics and my programming experience was typical of a mathematician.
Before using Isabelle/HOL, I was trying Coq, but the constructive way of
thinking in Coq is atypical in mainstream mathematics. Of course, there is
also a tradition of constructive mathematics for which Coq is fine (it is
also possible to do constructive mathematics in Isabelle, e.g., Isabelle/CTT).
For me, it was extremely easy to learn Isabelle/HOL without any course: I
only began to work in Isabelle/HOL as part of my Ph.D. program after
getting the skill in a left-taught way (to study many examples was
essential in this learning process).

Why as a person doing research in number theory I was interested in
learning Isabelle/HOL? The typical answer, that it is just to verify
whether or not current mathematical proofs in journals are correct, was not
my main motivation. For me, Isabelle/HOL was a sort of telescopy in order
to see deeper into my language-theoretic approach to number theory. Indeed,
using this approach, I was able to prove some number-theoretical
interesting results, e.g. I used my method explicitly here [3] and
implicitly here [4]. My goal at that time was to make the computer find new
theorems in an automatic way. I made some progress in the formalization of
the correspondence between number theory and language theory, but I stopped
because it was my own independent research and I changed to quantum
cryptography, a domain which is funded and where I am using Isabelle/HOL
motivated by cryptographical applications.

Concerning 3) I have two publications [1, 2], which, in my opinion, are as
human-readable as ordinary mathematics, for a mathematician with a
type-theoretic background. It is interesting to compare my formalization of
[1] with the original paper [6].

References
[1] Banach-Steinhaus Theorem:
https://www.isa-afp.org/entries/Banach_Steinhaus.html

[2] Arithmetic progressions and relative primes:
https://www.isa-afp.org/entries/Arith_Prog_Rel_Primes.html

[3] Jordan's Expansion of the Reciprocal of Theta Functions and 2-densely
Divisible Numbers: http://math.colgate.edu/~integers/u2/u2.pdf

[4] On a function introduced by Erdos and Nicolas:
https://www.sciencedirect.com/science/article/pii/S0022314X18301999

[5] Dyck words in Isabelle/HOL:
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory/tree/Dyck-(old-version)

[6]  Alan D. Sokal, A Really Simple Elementary Proof of the Uniform
Boundedness Theorem
https://www.tandfonline.com/doi/abs/10.4169/amer.math.monthly.118.05.450
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200513/554cd4c8/attachment-0001.html>