Thanks Morman, FL,
Proof minimization cost depends on how long we want/need to search. For a small proof it can be minutes, for larger proofs hours, and for some statements obviously we still, for now :), fail to find a proof in reasonable time despite them being provable with available axioms and definitions. We're happy to run our models on whichever list/benchmark you'd be interested in. Indeed, the models are trained on a particular version of set.mm, but note that these models are not really impacted by small changes to their training set. -stan On Sat, Mar 28, 2020 at 3:53 PM Norman Megill <[email protected]> wrote: > > Posted per FL's request. - Norm > > -------- Forwarded Message -------- > Subject: Stanislas' engine > Resent-From: nm > Date: Sat, 28 Mar 2020 14:53:18 +0100 (CET) > From: fl > To: Megill, Norman > > Hi Norm, > Could you ask Stanislas how long > dors it take to minimize a proof > and would it be possible to launcher > minimize_with and Stanislas' engine > to compare the results. And I > guess the neural network must > be made again for each new version > of set.mm, so how long does it take > to train the network. > > -- > 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/83b9299e-c8ac-49d3-9393-2700f04e59bc%40googlegroups.com. -- 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_0yP6EaiBW17zE4GT2GViUR2zOsLKFh-xkhnwMFjQaCrNA%40mail.gmail.com.
