Proposal: Categorizing Conjectures, Milestones, and SOTA Bou

Stream: Formal conjectures

[Kenta Kitamura]

Hi everyone,

Following the recent discussion in #Statement: Tao's lower bound for Lonely Runner, I’ve been thinking about how we can best organize these kinds of results as the repository grows.
(Such issues can be raised in large numbers for detailed intermediate theorems.)

As noted in the contribution guidelines, this repo encourages the formalization of not only open conjectures but also "solved variants of open conjectures and solved statements from dedicated problem lists."

To ensure the repository remains well-organized and to prevent confusion regarding the status of a problem, I’ve opened a formal proposal to implement a 3-tier classification system:

• Original Unsolved Conjecture: The primary open problem (e.g., the original LRC).

• Major Milestones: Solved statements that represent significant progress (e.g., Tao 2017 [arXiv:1701.02048]).

• SOTA Bounds: The most recent and strongest known results (e.g., Bedert 2025 [arXiv:2511.16636]).

Detailed proposal: https://github.com/google-deepmind/formal-conjectures/issues/1941

I believe this will help human contributors prioritize their efforts and provide better metadata for AI proof strategies. I would love to hear your thoughts on whether this kind of tagging would be a welcome addition to the workflow!

[Moritz Firsching]

Are you familiar with the categories we already have?

[Kenta Kitamura]

Yes — I looked at the current labels and they seem to cover (1) topic/AMS areas, (2) provenance (arXiv/OEIS/problem lists), and (3) workflow (WIP/needs-prerequisites/etc.).
My proposal is meant as an additional status layer orthogonal to those: original open conjecture vs major milestone results vs current best-known bounds.
To avoid conflicts, I’m happy to implement it with a status: prefix and align naming with existing conventions.

[Franz Huschenbeth]

I think the general goal of the project is to provide open problems, which serve as a benchmark for AI systems. The solved variants (and solved problems) act as an progression for judging how good a AI system is on a given problem and how good it can utilize the information from the literature to formalize the proof of the solved variant. In this vein only the categorization of open and solved is important any further information can be tracked via docstrings and variants I would say.

Tracking problem status is not the general goal of the project, but a small byproduct of maintaining its function of a proper benchmark consisting of open problems. Thats my view of the project, but I am open to be corrected.

[Moritz Firsching]

Probably still a good idea to add a label, or add a label which is called "new-theorem", to label those issues that propose to formalise a solved variant of a conjecture

[Franz Huschenbeth]

Moritz Firsching said:

Probably still a good idea to add a label, or add a label which is called "new-theorem", to label those issues that propose to formalise a solved variant of a conjecture

yeah, although formalization of novel new problems might be more bang for the buck from a benchmark perspective and I think we can still get a lot of such problems.

[Paul Lezeau]

Here it could be reasonable (and more consistent) for the issue tags we use to match the category attribute we use for the actual formalisation

[Franz Huschenbeth]

So you advocate to not introduce new issue labels? Or do you mean to extend the category attributes?

[Paul Lezeau]

I think it’s reasonable to have new issue labels: the suggestion was that these should match the category attributes. That way for example a person adding a statement with the category research open attribute would also have the corresponding label attached to the PR (or issue) and so on.

[Franz Huschenbeth]

Paul Lezeau said:

I think it’s reasonable to have new issue labels: the suggestion was that these should match the category attributes. That way for example a person adding a statement with the category research open attribute would also have the corresponding label attached to the PR (or issue) and so on.

So creating a "Open", "Solved" label? Should we just use "Solved" for solved progress variants or make an extra label then? I suppose you suggest to just use "Solved" when making a issue on a solved progress variant.

[Moritz Firsching]

I don't think the extra distinction between "solved" and "solved partial progress variants" is necessary. We have the two labels "new conjecture" and "formally solved elsewhere". So I propose add another label "new theorem" which corresponds to the cateogory "open". This could then be applied for instance to all issues that are concerend with solved Erdős problems.

We can discuss naming theses: Current state:

• "new conjecture": issues which become research category open
• "new theorem" (to be created): issues which become research category solved
• "formalisation exists elsewhere": issues which become research category formally solved using ...

I'd be wary to changing the label name "new conjecture" to just "open", because it might be confused with "open issue", no?

[Moritz Firsching]

Let's add "new theorem" as label?!

[Franz Huschenbeth]

Moritz Firsching said:

I don't think the extra distinction between "solved" and "solved partial progress variants" is necessary. We have the two labels "new conjecture" and "formally solved elsewhere". So I propose add another label "new theorem" which corresponds to the cateogory "open". This could then be applied for instance to all issues that are concerend with solved Erdős problems.

We can discuss naming theses: Current state:

• "new conjecture": issues which become research category open
• "new theorem" (to be created): issues which become research category solved
• "formally solved elsewhere": issues which become research category formally solved using ...

I'd be wary to changing the label name "new conjecture" to just "open", because it might be confused with "open issue", no?

"formally solved elsewhere"? Do you mean "F

Moritz Firsching said:

I don't think the extra distinction between "solved" and "solved partial progress variants" is necessary. We have the two labels "new conjecture" and "formally solved elsewhere". So I propose add another label "new theorem" which corresponds to the cateogory "open". This could then be applied for instance to all issues that are concerend with solved Erdős problems.

We can discuss naming theses: Current state:

• "new conjecture": issues which become research category open
• "new theorem" (to be created): issues which become research category solved
• "formally solved elsewhere": issues which become research category formally solved using ...

I'd be wary to changing the label name "new conjecture" to just "open", because it might be confused with "open issue", no?

I suppose we can explain the mapping to the category attributes in the label descriptions.

[Moritz Firsching]

Franz Huschenbeth said:

"formally solved elsewhere"? Do you mean "F

Yeah, I meant "formalisation exists elsewhere", will edit

[Franz Huschenbeth]

Moritz Firsching said:

Franz Huschenbeth said:

"formally solved elsewhere"? Do you mean "F

Yeah, I meant "formalisation exists elsewhere", will edit

Sorry, I thought I deleted the message :), I realized that you meant the "formalisation exists elsewhere" label.

[Moritz Firsching]

Moritz Firsching said:

Let's add "new theorem" as label?!

This is done now. Also added label description (limited to 100 characters by github..) to this one and "new conjecture"