Re: [isabelle] novice (first year undergrad) learning time



Will,

W.H. Billingsley wrote:
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 + k + 1) = fib(k + 1) * fib(n + 1) + fib(k) * fib(n)"

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.