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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and