student exercise: contributing to formal conjectures

Stream: Formal conjectures

[Floris van Doorn]

Hi!

@Michael Rothgang and I are teaching a Lean course in the fall semester. I am considering to add a large exercise/small project to ask the students to formalize their favorite conjecture and make a PR to formal-conjectures. Would this be welcome?

More details:

• This would entail approx. 30-60 PRs by relatively new Lean users (~1 month of experience)
• We will require that the formalization is carefully checked by another student before making a PR (hopefully lessening the reviewing burden)
• We will make sure there are 1-2 follow-up exercises to incorporate reviewer comments into their PR, so that the PRs don't get abandoned.
• Probably the PRs will actually come in ~2 months

For the students, this is good practice both in git and in Lean. It would be nice if these PRs get reviewed within ~1 week, if possible. It is very possible that some students will find this interesting, and voluntarily start making more PRs.

[Paul Lezeau]

Hi! That would be great - I'm quite happy to support this on the reviewing & merging side of things. Out of curiosity, have you already decided where these conjectures would be sourced? (or perhaps this will be left up to the students?)

[Floris van Doorn]

Great!
I think I would mostly leave it up to the students, but of course I can guide them by giving a couple of sources. Do you have suggestions for sources?

[Floris van Doorn]

Oh, one complication: I cannot force the students to sign the contributor license agreement with Google... I could still ask them to do this, and provide an alternative for the students that don't want to do this...

[Paul Lezeau]

Floris van Doorn said:

Great!
I think I would mostly leave it up to the students, but of course I can guide them by giving a couple of sources. Do you have suggestions for sources?

Re sources, I think conjectures from papers (arXiv/other places!) could be a good source, particularly for students that are interested in flavours of maths that don't appear too much in e.g. the Erdős problems list.

If that's helpful, we can set up an issue on the repo and add a few suggestions (this might also be helpful later to avoid duplication of work among the students!)

[Moritz Firsching]

That sounds great! We'd be happy to have the students contribute and will do our best to review these PRs quickly!

[Floris van Doorn]

Coming back to this: we're assigning the project this week, and ask the students to create a first version in 1-2 weeks, so expect some PRs from new contributors over the next weeks. There are about 40 students taking the class, and they can do this either alone or in pairs.

We cannot force the students to create a Google account / sign the contributor license agreement with Google. We will strongly encourage every student to do this and make a PR, but for the students that don't want to do this, they can make a PR to my fork of formal conjectures (in which case we will review the PRs).

[Moritz Firsching]

cool, looking forward to the contributions!

[Moritz Firsching]

Just of of curiosity, can you force the students to have a Github account?

[Floris van Doorn]

No. I will make special arrangements if a students doesn't want to create a GitHub account. This hasn't happened yet.
A Google account does feel a bit different, so there I will explicitly communicate an alternative option.

[Paul Lezeau]

For students that don't wish to sign the CLA/create a Google account, one alternative that @Michael Rothgang and I have discussed here would be the following:

1. The students open a PR, which is then reviewed and so on
2. Once the review process is complete, someone (e.g. me) opens a "shadow" PR referencing the original one with the student as a co-author (and adding their name to the list of formal-conjecture contributors if they are happy with that)

[Eric Wieser]

I'm not sure if the CLA permits that workaround

[Mauricio Collares]

Has DeepMind considered "donating" formal-conjectures to leanprover-community? The Lean community (unfortunately) doesn't use copyleft licenses, so that shouldn't be a problem.

[Mauricio Collares]

I can imagine a few strategic reasons why folks would want very tight control of the project, but I can't imagine people would deliberately break whatever CI checks are put in place to avoid incompatibilities with DeepMind internal use. Maybe it's possible to do it without changing maintainership?

[Moritz Firsching]

Mauricio Collares said:

Has DeepMind considered "donating" formal-conjectures to leanprover-community? The Lean community (unfortunately) doesn't use copyleft licenses, so that shouldn't be a problem.

I like this idea of moving formal-conjectures to the leanprover-community github organization! Especially when there is more contributions from outside Google DeepMind (which we hope very much to become more and more the case).

In any case, I hope the current requirements are not holding back too many people. While I can see that a teaching situation in a public university might be special/different, having CLAs in place for open source projects seems to be the norm. For instance tensorflow, chromium, android, keras, jax, alphafold, cirq all require a CLA and the CLA-signing for those also require a Google account (which can exclusively be used for that, I suppose).

[Moritz Firsching]

Mauricio Collares said:

I can imagine a few strategic reasons why folks would want very tight control of the project, but I can't imagine people would deliberately break whatever CI checks are put in place to avoid incompatibilities with DeepMind internal use. Maybe it's possible to do it without changing maintainership?

I wouldn't worry much about those incompatibilities, we could manage, I suppose, especially if maintainership is kept.