This looks very cool, thanks for posting about it here! I understand that the system has to be trained on a particular version of set.mm. It seems to me that it would not be that difficult to create a difference file that identified new theorems, and perhaps new definitions, that could be fed into this tool. Then it could automatically work on current versions of set.mm even though it had been trained on older versions.
Thoughts? --- David A.Wheeler -- 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/30A4B5BD-CE3E-45B6-A2B1-836F071A4EA4%40dwheeler.com.
