HomePage RecentChanges

port metamath to something our ai will like

I think that ghilbert may be even better for us, but it is not explicitly free. So one task is to

If it isn't free, we may want to do something similar, looking at the documentation, not at the code. Hmm. I expect the author will be reasonable.