33 New Proofs Found by Machines

[yangky11]

Hi,

We evaluated our machine learning prover on miniF2F and found 26 new proofs.

[spolu]

👏

[yangky11]

Hi,

I have re-run a new version of the model, which discovered 7 additional proofs: 5740c4a

[faabian]

Thank you for sharing the proofs! I'm not sure whether we should continue to add proofs to minif2f though because it will lead to training data contamination with Github being a classical source of pretraining data. I will leave it open for now :)

[yangky11]

I totally understand. Feel free to close this PR as you see appropriate.

[faabian]

Let's leave it open for visibility :)

[Adarsh321123]

@yangky11 What model did you use?

[ucalyptus2]

Hi @yangky11 , I have the same question as @Adarsh321123

[faabian]

I think this is the LeanDojo / ReProver paper: https://arxiv.org/abs/2306.15626

[yangky11]

I think this is the LeanDojo / ReProver paper: https://arxiv.org/abs/2306.15626

Yes, but we no longer maintain the Lean 3 model since people have switched to Lean 4.