Email Gateway (Aug 18 2022 at 10:12): Email Gateway (Aug 18 2022 at 10:12):From: "W.H. Billingsley" <whb21@cam.ac.uk>
How long do you reckon it would take a novice first year undergraduate (no
significant programming or proving experience) to learn to use
Isabelle/Isar well enough to complete induction or case proofs on the
Fibonacci sequence? For example, homework questions like Prove that "fib(n
I've found a few courses in Isabelle/HOL that seem to be aimed at the
postgraduate/researcher level, in either 8 * 90 mins or 4*90 mins sessions,
but I can't find much aimed at the first year level.
Sorry to ask a straw poll on the list, but there doesn't appear to be any
literature on this, and I'd like to get a rough idea.
cheers,
Will.
Email Gateway (Aug 18 2022 at 10:14):From: Robert Lamar <rlamar@stetson.edu>
Will,
W.H. Billingsley wrote:
Just last year, I was a fourth-year undergraduate performing a year-long
capstone project for my BSc in mathematics at Stetson University in
DeLand, FL, USA. A large portion of this project was figuring out how
to formalise a bit of ring theory in Isabelle/Isar. If it is helpful,
you may find the fruits of my labor at
http://www.macs.hw.ac.uk/~rob/docs/papers/rings.pdf .
The project was independent with weekly meetings with an adviser.
According to my memory, I started working through the Isabelle/HOL
system and reference manuals around the beginning of October 2005, and
didn't really feel comfortable with the system until February 2006. By
the end of November 2005, I had gathered enough ability to make a
semester's-end presentation to my department and compose a paper
summarising my progress.
If you are exploring the issues of a taught course for first-year
undergraduates, I would suspect that they could do simple things within
10 weeks. It might take as long as 20 weeks for an average student to
be proficient at the level you are suggesting. The trouble is that I
leaned on much of my undergraduate coursework (in both mathematics and
computer science) in grasping the concepts from Isabelle, Higher-Order
logic, and functional programming. If a student comes to the course
without that preparation, it is hard for me to guess the speed at which
they could move through the material. Another concern is that they have
the ability to do this sort of mathematics by hand. If you can't write
a proof for Theorem X in (say) English, you won't be able to prove it in
Isabelle.
If I may suggest, there is one important thing which should be impressed
upon these students. This is something I missed almost completely for
the longest time, but which is being corrected now in my work as a PhD
student. When one is trying to develop proofs in Isabelle and other
proof assistants, it is very desirable to model the proof structure upon
an existing, natural-language proof. For one reason or another, I got
it into my head that it would be a good idea for my Isar proofs to have
some semblance of originality. Looking back, I see that this was only a
hindrance to me, and potentially harmful to the exercise itself:
Formalised mathematics is best when it has an obvious relationship with
the original text. The student of proof who can grasp this is likely to
have a gentler experience.
I wish you well in the development of this course. I would be
interested in seeing the plan of instruction at which you arrive.
Robert Lamar
Email Gateway (Aug 18 2022 at 10:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes yes yes! A machine proof is much easier if you already understand
the intuition behind the traditional proof. It is a myth that
machine assistance can replace the need for competence and
understanding. The machine magnifies competence, but it also
magnifies incompetence...
Larry Paulson
Last updated: May 03 2024 at 12:27 UTC