I'm using miniF2F too. Great topic, thanks for the question Zheng and commentary Mario!
On Wed, Dec 21, 2022 at 3:05 PM Mario Carneiro <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/CAFXXJSs6xQE%3D_w_eNwQzG0nZQbTSRAttgx7QEUp_U_6epupTtg%40mail.gmail.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/CAHvyvqr9aQ4T4R_zmY_Lq8bc8m7zdiT8Hr_qBZBew0%3DkrkDOVA%40mail.gmail.com.
