License for models trained on CoqGym data

[tlringer]

Hi all,

I have a library that is currently MIT licensed, and I'd like to integrate a model trained on CoqGym data into that library. I'm curious what license you'd expect the library (or the relevant parts of the library) to have in that case. I care much more about establishing healthy community norms than the law, so I'm much more interested in your personal opinions and preferences than in what you expect the legal decision would be, especially since I think it's early enough that we can still set precedent in this community.

Thanks!

Talia

[yangky11]

Hi Talia,

Thanks for your interest in our work. You have raised a great question! I think license issues of trained models are very important and have generated a lot of discussions both within the research community and beyond. I do not have expertise in licenses and am still trying to learn more about the issues. I would be especially eager to learn from experts, and it would be great if you have any pointers. Thanks again for your question.

Best,

[brando90]

Curious, any progress on this?