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)

[Junyan Xu]

I thought proof_wanted is restricted to theorems with informal proofs that can readily be stated in Lean but formalizing the proofs is out of reach, not for unsolved / open problems, but apparently I misunderstood its scope. Shouldn't it be proof_or_disproof_wanted if used for statements we don't know is true or not? Now that there's the Formal Conjectures repo, should we move such statements there?

[Eric Wieser]

My impression was the proof_wanted for FLT was primarily a joke, if I'm remembering correctly that we even have one.

[Junyan Xu]

FLT is indeed a theorem after all? Are you implying my proof_wanted for Poincare conjecture / Perelman's theorem is also a joke?

[Junyan Xu]

If proof_wanted is for recognized theorems only, then a proof_wanted for $abc$ would be a joke.

[Eric Wieser]

I'd internalized that proof_wanted is for things where the proof isn't necessarily even that far out of reach, and the author wanted to commit to an API up front without actually proving it right now.

[Violeta Hernández]

Odd that you bring this up right after I proposed using proof_wanted to document an open problem in game theory!
https://github.com/vihdzp/combinatorial-games/pull/114#discussion_r2203628172

[Violeta Hernández]

I don't see the issue with using this for open problems. We want proofs of them! It's just that we might end up getting disproofs instead!

[Violeta Hernández]

Or is the idea that proof_wanted could be used in order to document where a new contributor might be able to help?

[Violeta Hernández]

In that case, I completely support making a new keyword with identical functionality but for open problems, could even be something like open_problem itself

[Edward van de Meent]

you could probably just make a macro for this, i don't see how there should be a semantic difference (to lean) between open_problem and proof_wanted

[Edward van de Meent]

proof of concept:

import Lean
import Batteries.Util.ProofWanted

open Lean Parser Elab Command

@[command_parser]
def «open_problem» := leading_parser
  declModifiers false >> "open_problem" >> declId >> ppIndent declSig

@[macro «open_problem»]
def foo : Macro
 | .node src ``«open_problem» #[mods,openproblem,id,sig] => pure <| Syntax.node src ``«proof_wanted» #[mods,mkAtomFrom openproblem "proof_wanted",id,sig]
 | _ => Macro.throwUnsupported

open_problem difficult : True

[Violeta Hernández]

I'd love to see this get added to Lean

[Edward van de Meent]

the easier/cleaner way to define this notation would be to edit the original proof_wanted in batteries, and keep the elab, but i don't know if batteries is open to supporting this?

[Violeta Hernández]

It probably doesn't hurt to make a PR.

[Edward van de Meent]

PR at batteries#1354

[Edward van de Meent]

as noted on the PR, apparently it would be preferrable to make the syntax itself extensible in some way rather than adding alternatives one at a time...
and my syntax-fu is not sufficient to make it work by adding a parser category...
should i try to PR a macro to mathlib, or maybe can we figure out a better syntax which mentions metadata in a sensible way?

[Eric Wieser]

This all feels like overkill right now vs just adding a comment

[Edward van de Meent]

yeah, although adding the syntax as a PR to mathlib doesnt seem too bad

[Edward van de Meent]

i.e. just the open_problem alias