Posted as requested. -------- Forwarded Message -------- Subject: AI and lemmas Resent-From: nm Date: Wed, 8 Apr 2020 20:39:33 +0200 (CEST) From:fl Reply-To: fl To: nm
Hi Norm, could you post this? If we have the intent of minimizing a proof with the AI engine, is it better to keep it in one chunk or can we divide it into several lemmas? -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4b4573bb-ce53-4485-b045-b47ad3875705%40googlegroups.com.
