Mario is right. They are meant to be commented out. (we were looking for a "canonical" way of commenting theorems in .mm file and finally we followed https://us.metamath.org/downloads/metamath.pdf section 4.4.1)
These are theorems without proof, so commenting out the theorems in this way makes it convenient to append all the pieces of metamath files from miniF2F to set.mm and then pass it to the checker. There is a more up-to-date version hosted by miniF2F where we include some more recent fixes with Albert Jiang and Wenda Li. https://github.com/facebookresearch/miniF2F Kunhao 在2022年12月22日星期四 UTC+8 04:05:12<[email protected]> 写道： > 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/cac915b1-6204-418c-af53-5228b0778d42n%40googlegroups.com.
