ProofNet ported in Lean 4

Stream: Machine Learning for Theorem Proving

[Rahul Vishwakarma]

I, along with @Abhijit Chakraborty have ported the ProofNet dataset statements into Lean 4: https://github.com/rahul3613/ProofNet-lean4

[Jason Rute]

I've talked about the need to benchmark all these powerful automatic tactics like Lean Copilot, duper, aesop, etc. This could be a good dataset for that (along with or in place of of MiniF2F). It would also be nice to benchmark the general-purpose automation tools that people regularly use like Github Copilot. (For example, @Alex Kontorovich recently said he finds GitHub Copilot more useful than Lean Copilot.)

[Jason Rute]

Also, how did you translate these? By hand? (Which would be ironic since they were generated automatically originally, right?) Or with Mathport? Or with an LLM?

[Rahul Vishwakarma]

We ported these statements manually, since we just wanted these statements in Lean 4 to evaluate the performance of our Lean 4 based automated theorem prover on this dataset.