I had a look at the metamath part of the miniF2F database (both https://github.com/openai/miniF2F/blob/main/metamath/test/aime-1983-p1.mm and https://github.com/facebookresearch/miniF2F/blob/main/metamath/test/aime-1983-p1.mm), but the syntax used there seemed strange. For example, it has "@e" instead of "$e" and "$@" instead of "$." Why is that? And has anyone actually checked that database?
-- 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/c423ea4d-d7b6-4698-b752-8130c5b9002fn%40googlegroups.com.
