Maintaining proof_wanted issues

Stream: Is there code for X?

[Fabrizio Montesi]

We can use proof_wanted to document theorems we want proven (#Is there code for X? > Documenting open problems). Has anybody tried integrating this with GitHub somehow?

For example, a GitHub action that, whenever a new proof_wanted theorem gets added to the repo:

• Creates an issue tagged 'Proof wanted' with description taken from the docstring of the theorem, unless an issue is already referenced from the docstring.
• If an issue is created, adds a link to the issue to the docstring of the theorem (commit & push).

(This could lead to adding some metadata to proof_wanted, but it's not strictly necessary.)

This would allow maintainers to collect & organise issues in github projects. Also, it'd allow people to declare that they're working on a (wanted) proof in the related issue on GitHub, fostering collaboration instead of duplicate work.

This is just a sketch for the sake of discussion, I haven't really thought it through yet.

[Fabrizio Montesi]

(A related discussion could be #Machine Learning for Theorem Proving > Incentives & sorry-filling leaderboard.)

[Yaël Dillies]

Stupid question: If a proof_wanted is modified/moved, how can automation identify this and avoid closing an issue to reopen another?

[Fabrizio Montesi]

We could look at the theorem name, I guess. handwaving reaches Italian level

[Fabrizio Montesi]

What's the emoji for 'actually not a stupid question'?

(resolved)

[Fabrizio Montesi]

This github action covers quite a bit of what we've discussed! https://github.com/marketplace/actions/todo-to-issue
But it requires using comments (/- TODO ... -/). Might be ok to do for now though...