License

Stream: Polynomial Freiman-Ruzsa conjecture

[Yaël Dillies]

Are contributors happy for their work on PFR to be made available under license Apache 2.0 (this is the one mathlib uses)?

[Yaël Dillies]

If no one objects by this weekend, I will add a license to the project and people who retroactively do not wish their work to be included under Apache 2.0 can make themselves known and we will add more precise copyrights to the files they contributed.

[Sean Welleck]

Hi all, we are making a new evaluation benchmark for machine learning-based provers that is based on recent Lean projects. The idea is to test a model's ability to prove theorems in a realistic setting (e.g., proving theorems that depend on the new definitions in a project).

We would like to include PFR, but there's currently no license; would it be possible to make the project available under Apache 2.0 or another license? I would also be happy to share our paper draft too if interested. Thank you!

[Yaël Dillies]

Sorry I was about to reply to your email but I had to revise for my final exam :grinning:

[Sean Welleck]

No problem, thank you!

[Yaël Dillies]

Added!

[Sean Welleck]

Thank you!!