Are lean proofs manually written or automatically found?

[fzyzcjy]

Hi thanks for the repo! As I am learning both lean and neural theorem proving, I am quite curious whether these proofs are automatically found? (For example, this long one: https://github.com/fzyzcjy/miniF2F/blob/5271ddec788677c815cf818a06f368ef6498a106/lean/src/valid.lean#L621-L681)

[DyeKuu]

Some of them are generated and some of them are written by humans. For example, this long one is written by humans.

[fzyzcjy]

@DyeKuu Thank you! Given https://arxiv.org/abs/2205.11491 says they solve ~40% of the problems (see screenshot), and this repo is owned by "facebookresearch", and README says "if you're using it and discovering new proofs (manually or automatically) please contribute them back to the benchmark", the conclusion seems that these solutions should be contributed to this repo ;)

[DyeKuu]

Yep, it is encouraged, and happy to see the contribution from the community but we do not want to enforce this to be mandatory :) I think you could open an issue to track this one.

[fzyzcjy]

@DyeKuu Sure, opened -> #10

Btw I am trying to reproduce this paper (though definitely does not have 230 A100 GPUs :/ ). I will contribute if I manage to automatically mine some proofs!

[venom12138]

@fzyzcjy Hi, how is your reproduce progress? Recently I am also working on ATP with MCTS. I would like to ask how you interact with the lean kernel (as the number of interactions increases, the efficiency of lean-gym developed by OpenAI will become lower and lower), btw, I would be very appreciative if you could public your code repository (even if it's still an on-going project.

[fzyzcjy]

@venom12138 Hi, seems someone was observing the same behavior - openai/lean-gym#24. I have not finished reproducing yet.