--
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/CAFXXJSsoNfduP5TgNbDzPMQEfFYYc4aCRt0y2aPRFPn6sH8ZyQ%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BCwN2q7qKqi5oh4WezRV75V%2BikgT9DJyT4_tbmO825yyQ%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuz8Q5Hxcu7U3iV6%3DU2KwwbWg6dhiJEVj5ZJSTHpayA_A%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJ48g%2BDNwi2KhpTfYh%2BgfSTYd%2BV33Qmr_hWNfLSn3O6OnfgBXQ%40mail.gmail.com.
Rather than shuffling which sounds complex, a simpler way to
verify that hypothesis might be to count the number of different
chapters/sections each theorem uses, and have a statistical
approach to confirm whether that matches with O(1) as Mario
suggests.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvYQQn1sDmjt1E_czs_vAuROUTTDVnWZpjC%3DjkaVSTWVA%40mail.gmail.com.
Is it ok to ask about your progress on MM0/MM1? Where have you got to with it, what have you been working on recently and where are you hoping to get to with it? I think it's awesome what you're doing with it and I'm interested to see what becomes of it. (I guess maybe this should be a new thread but I thought I would ask here).
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c1a69dcd-249e-40fc-b85c-ed62d5b4de0bn%40googlegroups.com.