Several lemmas is currently more amenable to minimization as the system is still very limited in its ability to work with longer proofs.
Hope this answers your question? -stan On Wed, Apr 8, 2020 at 10:10 PM Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/4b4573bb-ce53-4485-b045-b47ad3875705%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CACZd_0zaj3vLpFkLN0Tt2FLBf8KzZ-v9r8CGvJFJsftP19NPxw%40mail.gmail.com.
