*To*: Tjark Weber <webertj at in.tum.de>, Konrad Slind <konrad.slind at gmail.com>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 3 Jun 2012 23:44:22 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1338717861.1859.19.camel@weber> (message from Tjark Weber on Sun, 03 Jun 2012 12:04:21 +0200)*References*: <201206022353.q52Nredm012382@poisson.math.northwestern.edu> <1338717861.1859.19.camel@weber>

Thanks, Tjark and Konrad! I'll read the HOL paper, which looks pretty old, and so is maybe something that everyone just assumes nowadays. I don't know about those other first-order reasoning Automated_theorem_provers, or why folks don't use them. My interest in proof assistants (HOL Light, Isabelle, Coq) is that Tom Hales is using them to formalize his Kepler conjecture proof. it tends to puzzle mathematicians with an interest in foundations who have been taught that everything rests on FOL and ZFC. Tjark, you understand my confusion! Is something written about this? I do contend that it's true what mathematicians are taught, but it may not appear to be true at the technical level that proof assistants operate on. That's of course fine, but I need to see the underlying FOL and ZFC, even if the proof assistants aren't coded that way. -- Best, Bill

**Follow-Ups**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Ramana Kumar

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

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Tjark Weber

- Previous by Date: [isabelle] What are the atomic terms in Isabelle/HOL?
- Next by Date: Re: [isabelle] proof dags?
- 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 June 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