The pattern of using @e and so on is a common way of removing $ from metamath comments, enabling some basic nesting of comments. To restore the theorem you just run a regex find/replace over the comment contents.
The question then becomes, why are all the theorems commented out? Is it because they all have a proof by '?' ? It appears that the style was changed in https://github.com/openai/miniF2F/pull/1 but there is no discussion about this. I'm not aware of any checking that was done of these statements. Indeed, I have heard some bad things about the quality of the miniF2F database, see the discussion around https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Meta.20IMO.20result/near/312007122 . I'm somewhat skeptical of having OpenAI managing a database like this in the first place, it needs more community involvement to be robust and comprehensive. On Wed, Dec 21, 2022 at 1:20 PM Zheng Fan <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/c423ea4d-d7b6-4698-b752-8130c5b9002fn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs6xQE%3D_w_eNwQzG0nZQbTSRAttgx7QEUp_U_6epupTtg%40mail.gmail.com.
