*To*: "W.H. Billingsley" <whb21 at cam.ac.uk>*Subject*: Re: [isabelle] novice (first year undergrad) learning time*From*: Robert Lamar <rlamar at stetson.edu>*Date*: Wed, 21 Feb 2007 21:22:21 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <Prayer.1.0.18.0702192317390.3813@hermes-1.csi.cam.ac.uk>*References*: <Prayer.1.0.18.0702192317390.3813@hermes-1.csi.cam.ac.uk>*User-agent*: Thunderbird 1.5.0.9 (X11/20070102)

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 useIsabelle/Isar well enough to complete induction or case proofs on theFibonacci 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

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

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.

Robert Lamar

**Follow-Ups**:**Re: [isabelle] novice (first year undergrad) learning time***From:*Lawrence Paulson

**References**:**[isabelle] novice (first year undergrad) learning time***From:*W.H. Billingsley

- Previous by Date: [isabelle] post-doc position in Paris
- Next by Date: Re: [isabelle] generating isabelle theory files from ML modules?
- Previous by Thread: [isabelle] novice (first year undergrad) learning time
- Next by Thread: Re: [isabelle] novice (first year undergrad) learning time
- Cl-isabelle-users February 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list