> There is a more up-to-date version hosted by miniF2F EDIT: hosted by FAIR. FAIR also added informal descriptions to each statement in that repo. That might interest some NLP folks.
There is not yet a systematic checking, as far as I know: Sometimes errors are reported by researchers and we fix them. Since I left oai after my internship there ends and am focusing on my master program, I might not have the energy to take the lead. But I do believe checking from the experts in the formal math community is important and super valuable and would love to devote my time and find a way to contribute my efforts to that. Kunhao 在2022年12月22日星期四 UTC+8 10:00:59<Kunhao Zheng> 写道： > 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/8291b5ed-0fc2-4d7e-86f7-7efc6919fd05n%40googlegroups.com.
