[FOM] Re: Questions on proof assistants

[Wolfgang Windsteiger]

Hi everybody,

I totally agree with this. I think much of the problems are
"socio-cultural".

This is why I try to concentrate on bringing proof assistants to
students, not in particular but also to students who study to become
(math) teachers. As some of you know, I use the Theorema sysystem
(https://risc.jku.at/pj/theorema-project/), a system that has been
neglected by the whole community over the years. To a certain extent,
this is due to the fact that the system is based on Wolfram Mathematica,
and since a majority of the the proof assistant / automated reasoning
community has its roots in computer science they feel this as a hurdle.
However, for many mathematicians this is not such a big hurdle, since
many of them use Mathematica anyway. Yes, I know, there are other
systems, and there is commercial vs open source (sage etc.) etc. etc.
this is not what I'm aiming at here and now.

What I want to point out here is that Theorema by design gives proof
output that is human comprehensible. It does not need any translator,
nor an form of pretty printing, it gives proofs as written by a
mathematician genuinely. What Theorema is lacking are the really big
case studies of big important proofs having been carried out. True. And
the big libraries. True.

But for using the system in education (university,
undergraduate/graduate level in math&cs) this is still by far enough. I
have been using Theorema in teaching math/cs students over the years,
and usually Theorema can do the proof projects that I give to students
during and at the end of a semester without much effort. I give them
examples like "do the following proof by hand, then do the proof with
Theorema and compare your hand-proof with the automated proof coming
from Theorema, then do your proof again" and I ask for their experiences
then in an oral exam. Most interestingly, many students report that in
this way they found errors in their own proofs, and they like their
second version of the proof much more compared to their original proof.
For me, this "proves" that the Theorema output must be easily
comprehensible for humans.

Another hurdle for mathematicians is also a socio-cultural one: for
mathematicians a "proof" consists only of the tricky steps, the standard
steps are uninteresting. I fight since years against the habit of many
of my colleagues who mostly teach proof tricks that can be applied once
in a lifetime in one particular proof. And then they are proud to be
able to that one proof, and in the next proof they again need a once in
a lifetime hack. They educate masters of proof tricks, who then sadly
fail in the "trivial" parts of the proofs, when they mix up "arbitrary
but fixed" with "instantiation", or when they infer new knowledge from
something that needs to be proved, etc. etc. you know all this. In this
ecosystem, it is of course a hard terrain for proof assistants, for them
they do not assist, they are in their way ...

Maybe you find it worthwile to look at Theorema once, you find pointers
on the webpage above. As for the case studies: we did a (bigger) case
study in auction theory with a (I think) nice comparison of the
formalization in Theorema compared to the formalization in Isabelle.
This work was presented at CICM'2017, see below.

I must say, I was very happy to see that comprehensibility by humans
seems to become more of a topic when I read the original post in this
thread.

Greetings,
ciao,
WW.

@inproceedings{RISC4536,
author = {A. Maletzky and W. Windsteiger},
title = {{The Formalization of Vickrey Auctions: A Comparison of Two
Approaches in Isabelle and Theorema}},
booktitle = {{Intelligent Computer Mathematics: 10th International
Conference, CICM 2017, Edinburgh, UK, July 17-21}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10383},
pages = {25--39},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-62075-6},
year = {2017},
note = {doi 10.1007/978-3-319-62075-6_3},
editor = {H. Geuvers and M. England and O. Hasan and F. Rabe and O.
Teschke},
refereed = {yes},
length = {15},
url = {https://link.springer.com/chapter/10.1007/978-3-319-62075-6_3}
}

On 14.05.20 12:35, Christoph Benzmueller wrote:
> Generally, I do not believe anymore that senior mathematicians can easily
> be converted to fruitfully work with proof assistants. It is rather the
> younger generation of interdisciplinary trained young researchers (maths,
> CS, philosophy) that we should focus on. And if these younger researchers
> then cooperate with senior researchers in formalisation works, some real
> progress can be expected.

-- 
Assoc.Univ.-Prof. DI Dr. Wolfgang Windsteiger
RISC Institute / JKU Linz
Castle Hagenberg, 4232 Hagenberg i.M., Austria
Phone: +43 732 2468-9960
http://www.risc.jku.at/home/wwindste/
PGP: find the public key on my homepage

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: </pipermail/fom/attachments/20200515/306e6207/attachment-0001.asc>