Re: [isabelle] Isabelle Foundation & Certification



On Sat, 2015-09-19 at 11:38 +0200, Tjark Weber wrote:
> But if someone gives you an Isabelle theory and claims that it proves,
> e.g, FLT, there is no machine that could decide this claim for you.

To elaborate, and to answer questions that I received via private
email: The main difficulty here is that Isabelle theories are written
in a rich and powerful language (that may contain, e.g., embedded ML
code), to the point that the observable behavior of Isabelle when it
checks (or more accurately, processes) the theory cannot be trusted.

Of course, other theorem provers with powerful proof languages also
suffer from this problem.

Best,
Tjark






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