*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] question*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Sat, 25 Jan 2014 13:48:13 +1300*In-reply-to*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11 at cantab.net>*References*: <866E7D87-1D8F-459E-808D-3DDE9D30EA11 at cantab.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

For my Master's thesis, I formalized in Isabelle a proof of the independence of the equivalent of the parallels postulate in Tarski's axioms of geometry [1]. That would have been far too big to do by hand first (at least at the speed I write). But when I couldn't easily keep a part of the proof in my head all at once, I'd draw myself a map of which lemmas were required to prove which other lemmas, and then I could concentrate one at a time on any lemma such that all of the lemmas it depended on had already been formalized. I've attached a couple of examples. Having said that, I did do pen-and-paper working for some of the lemmas mentioned on those pages, though many of them went straight from my head into Isabelle, probably including some that were never even mentioned on the map. This suited my style well, but I suspect that the best strategy is highly dependent on the style of the person using it. For me, I naturally tend to write proofs in more detail than most, so writing proofs for Isabelle wasn't as much of a hurdle as it probably is for some other people. And I grew up with computers, too; I often feel more comfortable writing a letter on a computer, rather than writing it by hand, but some people prefer to write by hand first, even if they're going to type up the result in the end. Tim <>< [1] http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml On 25/01/14 05:54, John Wickerson wrote: > Hi all, > > I wonder if I might invite comment on the following statement? > > "Don't even *think* about firing up Isabelle until you've completed a really solid pencil-and-paper proof of the theorem you want to mechanise." > > Thanks! > John >

**Attachment:
IMG_20140125_125138.jpg**

**Attachment:
IMG_20140125_125401.jpg**

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Enter MATCH
- Next by Date: Re: [isabelle] Enter MATCH
- Previous by Thread: Re: [isabelle] question
- Next by Thread: Re: [isabelle] question
- Cl-isabelle-users January 2014 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