Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Minif2f ported to Lean 4


Zhangir Azerbayev (May 03 2023 at 21:23):

On huggingface.

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

Eric Wieser (May 03 2023 at 21:56):

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

Albert Jiang (May 04 2023 at 08:51):

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 (May 28 2023 at 05:20):

@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 :-)


Last updated: Dec 20 2023 at 11:08 UTC