Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.