miniF2F database

[Zheng Fan]

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?

[Mario Carneiro]

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 <fanzhe...@outlook.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c423ea4d-d7b6-4698-b752-8130c5b9002fn%40googlegroups.com.

[Johnathan Mercer]

I'm using miniF2F too. Great topic, thanks for the question Zheng and commentary Mario!

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs6xQE%3D_w_eNwQzG0nZQbTSRAttgx7QEUp_U_6epupTtg%40mail.gmail.com.

[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

[Kunhao Zheng]

>  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