Re: [isabelle] rigorous axiomatic geometry proof in Isabelle (Bill Richter)

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.


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