Fwd: AI and lemmas
41 views
Skip to first unread message
Norman Megill
Apr 8, 2020, 4:10:16 PM4/8/20
to Metamath
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
-------- 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
Stanislas Polu
Apr 8, 2020, 4:17:32 PM4/8/20
to meta...@googlegroups.com
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
--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4b4573bb-ce53-4485-b045-b47ad3875705%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages