Re: [isabelle] Verify the legitimacy of a proof?



On 08/07/2017 12:46, Makarius wrote:

HOL-Zero is a notable exception in targeting a market of potentially
malicious (ab-)users, but it is not a "big prover".

Yes, and it is mainly intended to be used as a proof checker, via proof objects. You export your formal proof as proof objects, then import these into HOL Zero. In this sense it is perfectly capable - it has successfully checked in one session of a few hours the 1.4 billion primitive inference steps of 2 of the 4 parts of Flyspeck (the main text and the linear inequalities).

Mark.




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