search

facebookresearch / miniF2F

An updated version of miniF2F with lots of fixes and informal statements / solutions.
MIT License
60 stars 19 forks source link

33 New Proofs Found by Machines #13

Open yangky11 opened 1 year ago

yangky11 commented 1 year ago

Hi,

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

yangky11 commented 1 year ago

Hi,

I have re-run a new version of the model, which discovered 7 additional proofs: https://github.com/facebookresearch/miniF2F/pull/13/commits/5740c4ac7978a97b25a747c5ade52f896edce1f7

faabian commented 1 year ago

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 commented 1 year ago

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

faabian commented 1 year ago

Let's leave it open for visibility :)

Adarsh321123 commented 3 weeks ago

@yangky11 What model did you use?

ucalyptus2 commented 1 day ago

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

faabian commented 1 day ago

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

yangky11 commented 1 day ago

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.