Documenting open problems

Stream: Is there code for X?

[Tristan Figueroa-Reid]

I was looking at an old open problem that @Violeta Hernández noticed when formalizing Game birthdays (https://github.com/leanprover-community/mathlib4/blob/2d4a40714ede518ac0e07965d3145ad9209b2537/Mathlib/SetTheory/Game/Birthday.lean#L269-L270) and I was wondering: is there any standard way to document open problems that are naturally defined and accepted in literature? From a quick few greps, I haven't noticed anything like this at all.

[Kim Morrison]

There is proof_wanted.

[Tristan Figueroa-Reid]

Interesting! Would it be acceptable to write PRs that tag easily definable and relevant open problems with proof_wanted?

[Kim Morrison]

Yes, I think so. Note that so far proof_wanted has not been a resounding success, but this is mostly through lack of people using it, rather than any structural problem we've identified with the idea.

[Tristan Figueroa-Reid]

That's really good to know! Since combinatorial game theory is a relatively undeveloped field, there's a good chance anyone working there will hit a lot of small open problems in the upcoming years.

[Alok Singh]

Kim Morrison said:

Yes, I think so. Note that so far proof_wanted has not been a resounding success, but this is mostly through lack of people using it, rather than any structural problem we've identified with the idea.

be the change you wanna see?

[Tristan Figueroa-Reid]

(I think there are more resounding issues than proof_wanted), though I absolutely don't mind tagging any open problems that are easy to define with proof_wanted :+1:

[Tristan Figueroa-Reid]

Is there any tool that makes it easy to see proof_wanted/sorry calls across various lean codebases? *Also, if there's already a Zulip thread for this, I can move the conversation there.

[Kim Morrison]

See the discussion at #Machine Learning for Theorem Proving > Incentives & sorry-filling leaderboard , in particular my suggestions and Lenny Taelman's implementations.

[Tristan Figueroa-Reid]

Also, it would be nice if proof_wanted had attributes/metadata that indicated if something was an open problem, or if the theorem with a desired proof might be false.

[Violeta Hernández]

I've opened #21155 turning my comment into a proof_wanted block.

[Tristan Figueroa-Reid]

An image of the added changes from the #21155 pull request. The ⨳ unicode symbol is overflowing the line it is in, and it does not have the usual green overlay that the rest of GitHub's diffs do when displayed.
I did not know that ⨳ does not play well with GitHub's diff view!

[Violeta Hernández]

Do note that the Math Overflow question was exclusively about surreals, whereas this formulation is for arbitrary games. Pre-game multiplication is mostly meaningless for non-surreal games, so there might be some weird counterexample by just substituting random values.

[Violeta Hernández]

I don't think we currently have any file that imports both birthdays and surreals, though

[Violeta Hernández]

Quick sanity check: what happens if we substitute the games * and *' as defined in https://leanprover-community.github.io/mathlib4_docs/Counterexamples/GameMultiplication.html?

[Violeta Hernández]

...I think the sanity check fails

[Violeta Hernández]

If I'm not mistaken, star * star' ≈ nim 2

[Violeta Hernández]

Which means that two games with birthday 1 multiply to a game with birthday 2

[Tristan Figueroa-Reid]

(Also, I wonder if PGame could have some form of shrinkwrap testing for short PGames - I believe there's a tool for this in lean4, right?)

[Violeta Hernández]

There was this note on the Short.lean file about how by decide wasn't actually working. This is from Lean 3 and I don't think the file has been meaningfully touched since.

[Tristan Figueroa-Reid]

Right; I forgot decidability is necessary for that.

[Violeta Hernández]

We really should do the proposed Short refactor before this, though

[Violeta Hernández]

What should I do with my comment now that it turns out that the only version of the theorem we can state within the file is wrong?

[Tristan Figueroa-Reid]

A file in Counterexamples and a subsequent proof_wanted declaration in Surreal.lean would be nice since it is still an open problem for Surreals.

[Violeta Hernández]

Surreal.lean doesn't import Birthday.lean though. That being said it wouldn't be a huge import increase given that it already imports ordinals... even though it probably shouldn't?

[Violeta Hernández]

I think this should be discussed in another thread.

[Kim Morrison]

Tristan Figueroa-Reid said:

Also, it would be nice if proof_wanted had attributes/metadata that indicated if something was an open problem, or if the theorem with a desired proof might be false.

I think we should start by asking for comments, and if we ever get to the point of having many proof_wanteds with interesting comments, we can think about how to convert those comments into metadata.

[Tristan Figueroa-Reid]

(moved to relevant thread)