*To*: Jeremy Avigad <avigad at cmu.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Tue, 1 May 2012 20:56:25 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F9FE203.6050907@cmu.edu> (message from Jeremy Avigad on Tue, 01 May 2012 09:15:47 -0400)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAPeE+xWo7_cfF6UE_P9OpD_Ot1iBQ-_OApymFyvXPF458Qw+fQ@mail.gmail.com> <201204292118.q3TLI5TK018411@poisson.math.northwestern.edu> <4F9F1B2B.1020209@gmail.com> <201205010456.q414uPRf032246@poisson.math.northwestern.edu> <4F9FE203.6050907@cmu.edu>

Jeremy, I'll look at your paper, but don't want to discuss Euclid with you or anyone else here unless they understand Hilbert's formal (not informal) first order axiomatization of plane geometry as explained in Hartshorne's book: 3 incidence axioms, 4 betweenness axioms, 6 congruence axioms, the parallel postulate and the circle-circle axiom. With these axioms, you can prove every plane geometry result Euclid stated, and you ought to be able to code the proofs up nicely in Isabelle, and maybe even teach a high school or college course where the students code up their own rigorous axiomatic Hilbert proofs. You can't code up proofs of Euclid's propositions using Euclid's axioms. Your paper is relevant to this group if you can code up your enhanced-Euclid proofs in Isabelle. I couldn't tell from my brief glance at your paper if this is possible. What do you think? -- Best, Bill

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tim (McKenzie) Makarios

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Jeremy Avigad

- Previous by Date: Re: [isabelle] Linear Ordering for nat list
- Next by Date: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Next by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
- Cl-isabelle-users May 2012 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