Email Gateway (Aug 22 2022 at 19:13): Email Gateway (Aug 22 2022 at 19:13):From: "Pal, Abhik" <ab.pal@jacobs-university.de>
Dear all,
I'm writing on behalf of the Hilbert-10 workgroup at Jacobs
University, Bremen --- a small team of second-year undergraduate
students working on a formalization of Yuri Matiyasevich's proof of
Hilbert's Tenth problem in Isabelle.
We are trying to consolidate our experience of working on a theorem
prover as a submission to CICM [1]. In our submission we don't tackle
the formalization but reflect on the process itself. In particular, we
discuss how we as a group of inexperienced undergraduates with no
prior theorem proving experience decided to tackle the formalization
of a non-trivial mathematical result.
Hence, we are interested in hearing your experience of learning to use
a theorem prover. In particular, we're interested in
your academic background when you learnt to use a theorem prover.
What parts of your formal education made it easier to actually
understand theorem proving?
in retrospect, what were the gaps in knowledge you had when you got
started?
what were the common mistakes you made? What concepts were difficult
to understand?
anything else about the experience of learning a theorem prover.
Broadly, we would also like to use this as an opportunity to generate
a discussion around the usability of theorem provers themselves and
making them more accessible.
We would love to know what you think!
Abhik
[1]: Tentative abstract:
How difficult are theorem provers to use for beginners? We
respond by reviewing the formalization of the DPRM theorem in
Isabelle carried out by an undergraduate research group at Jacobs
University, Bremen. We argue that theorem provers are feasible.
However, we also survey the factors that keep beginners from
using them effectively and propose specific measures to make the
field more accessible to new users. Broadly, we advocate for an
increased adoption and regular use of theorem provers in
mathematical research.
0xBC35C23EB221FB65.asc
signature.asc
Email Gateway (Aug 22 2022 at 19:13):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello Abhik,
It is a pleasure to share my experiences about learning Isabelle/HOL
(below: Q for Question and A for Answer). Please correct my English if
there are some mistakes.
Q: Your academic background when you learnt to use a theorem prover.
A: I learned Isabelle/HOL, in a self-taught way (from the manuals), having
a Master degree in Pure Mathematics. Before that, I learned Coq, again in a
self-taught way (from the manuals).
Q: What parts of your formal education made it easier to actually
understand theorem proving?
A: A course on Formal Set Theory given by Prof. Alexander Shnirelman at
Concordia University.
Q: In retrospect, what were the gaps in knowledge you had when you
got started?
A: Type Theory was the main gap. In general, it is not part of the
background in Pure Mathematics. I learned homotopy type theory from the
video-lectures given by Robert Harper. My access to these lectures was by
means of YouTube.
Q: What were the common mistakes you made?
A: The main mistakes were related to the types, e.g., (1::nat) is not the
same as (1::real). This was, again, because of the lack of background in
type theory. Nevertheless, it was easy to get used to this new way of
thinking.
Q: What concepts were difficult to understand?
A: For me, the most difficult concept to understand was the difference
between dependent type theory (Coq) and simple type theory (Isabelle/HOL).
When someone learns Coq first, he/she tries to work in the same way in
Isabelle/HOL, but this is counterproductive. Isabelle/HOL deserves its own
way of thinking. So, I recommend to learn Isabelle/HOL first and then Coq.
Q: Anything else about the experience of learning a theorem prover.
A: I think that the best way to begin to practice Isabelle/HOL is to do
elementary number theory, e.g., to prove Bezout's Identity, Fermat's Little
Theorem, Wilson's Theorem, etc. These results can be easily formalized. It
is important to understand the mathematics before to begin the
formalization: never formalize something that you do not understand. It is
important to begin with the statement of the theorem and then to prove it
under the assumption that some lemmas are proved (use the keyword "sorry"),
and repeat this process until the end. Finally, take coffee naps of 20-30
minutes every 4 hours, it eliminates brain fatigue (don't fear the
nosebleed, in most cases, it does not come from the brain).
Sincerely yours,
José Manuel Rodriguez Caballero
https://www.researchgate.net/profile/Jose_Rodriguez_Caballero2
Email Gateway (Aug 22 2022 at 19:13):From: Makarius <makarius@sketis.net>
The problem is also the use of the same words for slightly different
things. The difference of "dependent type theory" vs. "simple type
theory" is not just in "dependent" vs. "simple", but also in "type
theory" vs. "type theory".
Even Coq and HOL experts can get fooled by this. There are very few
people who know both worlds sufficiently well to understand this
misunderstanding.
Makarius
Email Gateway (Aug 22 2022 at 19:13):From: Makarius <makarius@sketis.net>
Hopefully many Isabelle users will provide you some input for the paper.
Such experience reports are very important for the progress of the
prover communities.
CICM is a good place for such "soft" contributions, beyond the hard
formalizations. (Note that I will be there myself this year, as an
invited speaker of the MKM track.)
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 19:13):From: Freek Wiedijk <freek@cs.ru.nl>
Dear Makarius,
I don't know what the difference is, these strings seem
identical to me :-) Let's see:
% ocaml
OCaml version 4.06.1
%
Ah no, you're right, they _are_ different! (And apologies
for running OCaml 4.06.1 instead of 4.07.0, this has
something to do with a project that I am in which is at
some version of VST. I think.)
For me the difference between Isabelle's type theory ("simple
type theory") and Coq's type theory ("dependent type theory")
is that in the first you have a unified framework in which
terms and formulas are the same thing (typed lambda terms),
while in the second, the terms, formulas _and_ proofs are
all the same kind of thing (again: typed lambda terms).
So the main difference is the use in dependent type theory of
the Curry-Howard isomorphism, and the resulting possibility
for functions to take "proof objects" as arguments.
For example, in Coq the division operator (for an appropriate
version of division) takes _three_ arguments: x, y, and
a proof that y <> 0. This means that the term 0/0 is a
_function,_ from proofs of 0 <> 0 to numbers.
Freek
Email Gateway (Aug 22 2022 at 19:14):From: Makarius <makarius@sketis.net>
On 22/02/2019 18:38, Freek Wiedijk wrote:
The problem is also the use of the same words for slightly different
things. The difference of "dependent type theory" vs. "simple type
theory" is not just in "dependent" vs. "simple", but also in "type
theory" vs. "type theory".% ocaml
OCaml version 4.06.1"type theory" == "type theory";;
- : bool = false
Nice illustration :-)
For me the difference between Isabelle's type theory ("simple
type theory") and Coq's type theory ("dependent type theory")
is that in the first you have a unified framework in which
terms and formulas are the same thing (typed lambda terms),
while in the second, the terms, formulas _and_ proofs are
all the same kind of thing (again: typed lambda terms).
You wrote "Isabelle" and probably meant the Isabelle/HOL library.
Isabelle as a logical framework was invented by Larry Paulson to
formalize variants of Martin-Löf Type Theory. In restrospect it might be
interesting to look what was missing to make this really work out: the
Isabelle/HoTT threads on this mailing list could be a starting point for
that.
Coq users typically develop a certain mindset of what a "type" is and
how it is used in formalizations: it is more about logic than about
classic use of types for abstract syntax. E.g. when a Coq user says
"type checking" (for "proof checking"), a HOL user will usually
misunderstand that as a false-friend.
So the main difference is the use in dependent type theory of
the Curry-Howard isomorphism, and the resulting possibility
for functions to take "proof objects" as arguments.For example, in Coq the division operator (for an appropriate
version of division) takes _three_ arguments: x, y, and
a proof that y <> 0. This means that the term 0/0 is a
_function,_ from proofs of 0 <> 0 to numbers.
In such situations I am often glad that HOL cannot do this. Cf. the
parallel thread on the HOL mailing list about "0 / 0 = 0 ???".
Makarius
Email Gateway (Aug 22 2022 at 19:14):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Abhik and team,
first of all congratulations on your initiative and your very
interesting work.
I attended a presentation on your project back in July in Oxford- it
looks like you are doing a great job.
Right now I am also in the process of writing a "beginner's experience"/
review report on my Isabelle experience,
and I can share it with you when I finish it, if you like.
(I started using Isabelle a bit over a year ago, working in Lawrence
Paulson's ALEXANDRIA project at the University of Cambridge, and I got
my PhD in pure Mathematics around 2 years ago)
Best wishes,
Angeliki
Dr Angeliki Koutsoukou-Argyraki
Research Associate
Fellow of St Edmund’s College
Computer Laboratory
15 JJ Thomson Avenue
University of Cambridge
CB3 0FD, UK
ak2110[at]cam[dot]ac[dot]uk
https://www.cl.cam.ac.uk/~ak2110/
Last updated: Nov 21 2024 at 12:39 UTC