Hi Mario, that was a nice talk, your work is very interesting. Can I ask about classic search to produce metamath proofs? You say MM0 is a lot quicker and is not yet parallelised as that is not required at the moment. I find it a bit hard to work out the branching factor for an MM proof, I imagine it is quite high, however if you parallelised your system how many steps deep do you think you could get with a breadth first search? Even a search that could do 3 or 4 steps deep might be powerful for speeding up proving things.
Anyway thanks it was interesting. -- 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/e3220a38-730b-48ab-9d74-e316c99ef874%40googlegroups.com.
