Minif2f ported to Lean 4

Stream: Machine Learning for Theorem Proving

[Zhangir Azerbayev]

On huggingface.

Ported by @Sean Welleck. A few formal statements are commented out because logarithms aren't ported yet.

[Eric Wieser]

Presumably this is generated output from a source repository that contains Lean files? Which version of miniF2F was this ported from?

[Albert Jiang]

Zhangir Azerbayev said:

On huggingface.

Ported by Sean Welleck. A few formal statements are commented out because logarithms aren't ported yet.

Great work!!! Can you open a PR at https://github.com/facebookresearch/miniF2F/pulls? They can merge very quickly :)

[Scott Morrison]

@Zhangir Azerbayev, is there a repo with issue tracking? I found at least one error... (by watching GPT try the obvious proof and have it not work :-)