*To*: "Luke Serafin" <lserafin at andrew.cmu.edu>*Subject*: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Fri, 15 Jun 2012 22:28:59 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <21f54a2415554d519851b44b5df2abff.squirrel@webmail.andrew.cmu.edu> (lserafin@andrew.cmu.edu)*References*: <mailman.49963.1339656957.29855.cl-isabelle-users@lists.cam.ac.uk> <21f54a2415554d519851b44b5df2abff.squirrel@webmail.andrew.cmu.edu>

Thanks, Luke! Thanks for recommending TTTP. You're not addressing my position, that of a typical mathematician inflamed by Tom Hales's attempt to formalize his proof of the Kepler sphere-packing conjecture with HOL Light, Coq and Isabelle. Folks like me know some math logic, meaning FOL+ZFC, and they want to know how to translate this to what are no doubt more useful and more practical things like HOL & Isar. -- Best, Bill

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

- Previous by Date: [isabelle] New commands in Isabelle2012
- Next by Date: Re: [isabelle] New commands in Isabelle2012
- Previous by Thread: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)
- Next by Thread: Re: [isabelle] Looking for the GOOD way to use Isabelle and Latex together when writing a thesis
- 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