Proposal: Classification and Tagging for Original Conjectures, Milestones, and SOTA Bounds

## Background
According to the [contribution guidelines](https://github.com/google-deepmind/formal-conjectures#id-like-to-contribute---what-can-i-do), this repository encourages the formalization of not only open conjectures but also **"solved variants of open conjectures and solved statements from dedicated problem lists."**

As the repository grows, I believe it is essential to establish a clear tagging or classification system to distinguish between original targets and these solved variants. Without this, there is a risk of confusion for contributors regarding the current status of a problem.

## The Proposal: A 3-Tier Classification
To ensure human contributors and AI agents use their resources effectively, I propose categorizing statements into three distinct types:

1. **Original Unsolved Conjecture:** The primary open problem.
2. **Major Milestones / Significant Progress:** Solved statements or reformulations that contributed strongly to the progress of the original conjecture.
3. **State-of-the-Art (SOTA) Bounds:** The most recent and strongest known results (even if proven).

### For Example: Lonely Runner Conjecture (LRC)
We can see the necessity of this distinction in the LRC case:
- **Type 1:** The original Lonely Runner Conjecture (unsolved).
- **Type 2:** **Tao's 2017 result** [arXiv:1701.02048] (A major milestone/improved bound). This is similar to how Frey’s Theorem serves as a milestone for FLT.
- **Type 3:** **Benjamin Bedert's 2025 result** [arXiv:2511.16636] (The current SOTA bound).

## Benefits
- **Contributor Efficiency:** Formalizers can immediately know if they are tackling an open mystery or a proven milestone.
- **AI-Ready Metadata:** Provides crucial context for AI tools to distinguish between "unproven" statements and "proven but unformalized" theorems, allowing for better proof strategy selection.
- **Organization:** Prevents "issue spam" by providing a clear framework for how variants should be proposed and tagged.

I would love to hear the thoughts on adding labels such as `status:original`, `status:milestone`, or `status:SOTA` to support this workflow.

Start with the contribution guidelines linked in the issue and review the proposed Lonely Runner Conjecture examples. Compare the three categories against how statements are currently described, then document the agreed classification and labels if maintainers approve the proposal.

Written by the indexing model from the issue text.