[isabelle] An ATP question

Hi I would like to know if anyone has tried converting Isabelle/ZF or even
Isabelle/HOL proofs to Metamath format and then using an evolutionary
algorithm or any other search algorithm for automatic proving, to be used
with Sledgehammer?


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