Status-colors
# Status Colors Explained
Every declaration in a Side-by-Side Blueprint site is assigned a status that reflects its formalization progress. Status is shown as colored dots next to declaration names on the dashboard, in chapter pages, and in the dependency graph.
## The Seven Statuses
### Not Ready (Orange)
The declaration exists in the LaTeX document but has no Lean implementation yet. This is the default starting state for every declaration. It means the mathematical statement has been written informally, but no one has begun formalizing it in Lean.
Think of this as: "We know what we want to prove, but haven't started writing Lean code."
### WIP (Teal)
The declaration is actively being worked on. This is a manually set status -- the author marks a declaration as "wip" to signal that formalization is in progress. This replaces the former "ready" status with clearer intent.
Think of this as: "Someone is actively working on this."
### Sorry (Red)
The Lean code contains `sorry`, which is Lean's placeholder for incomplete proofs. The system detects this automatically. A sorry status means someone has started working on the proof but has not finished it, or has intentionally left a gap.
Think of this as: "Work in progress -- there are holes in the proof."
### Proven (Green)
The proof is complete -- no `sorry` remains in the Lean code, and the declaration typechecks. However, some of the declarations that this one depends on may still be incomplete. A proven declaration is locally correct, but the full logical chain may have gaps elsewhere.
Think of this as: "This proof is done, but it might rely on things that aren't done yet."
### Fully Proven (Dark Green)
The strongest status. The proof is complete AND every declaration it depends on (transitively) is also proven. This means the entire logical chain from foundational axioms to this declaration is verified end-to-end. The system computes this automatically by traversing the dependency graph.
Think of this as: "This result is fully verified -- nothing it depends on is missing."
### Axiom (Purple)
The declaration is a Lean `axiom` -- an intentionally unproven assumption. Unlike `sorry`, axioms are structural choices, not gaps. The system detects this automatically from the declaration type.
Think of this as: "This is an assumed foundation, not a missing proof."
### Mathlib Ready (Blue)
A manually set status indicating the declaration is ready for submission to Mathlib, the community library of formalized mathematics for Lean 4. This is the author's signal that the code meets Mathlib's quality and style standards.
Think of this as: "This is polished and ready to contribute upstream."
## How Status Progresses
A typical declaration moves through these stages as work advances:
```
Not Ready --> WIP --> Sorry --> Proven --> Fully Proven
(orange) (teal) (red) (green) (dark green)
```
1. You write the LaTeX statement. The node appears as **Not Ready**.
2. You begin formalizing. The author marks it **WIP**.
3. You write the proof with `sorry` placeholders. It becomes **Sorry**.
4. You complete the proof. It becomes **Proven**.
5. Once all its dependencies are also proven, the system upgrades it to **Fully Proven**.
At any point, the author may mark it **Mathlib Ready** to indicate it is polished for contribution. Lean `axiom` declarations are automatically shown as **Axiom** (purple).
## Automatic vs. Manual
Four statuses are detected automatically by analyzing the Lean code:
| Status | Detection |
|--------|-----------|
| Sorry | Code contains `sorry` (the `sorryAx` axiom) |
| Proven | Code is complete with no `sorry` |
| Fully Proven | Proven, and all transitive dependencies are also proven |
| Axiom | Declaration is a Lean `axiom` (intentionally unproven) |
Two statuses are set manually by the project author:
| Status | When to Use |
|--------|-------------|
| WIP | Actively being worked on |
| Mathlib Ready | Code is ready for Mathlib submission |
Not Ready is the default status for declarations without Lean code. Manual flags take priority over automatic detection. For example, if a proven declaration is marked `mathlibReady`, it displays as Mathlib Ready (blue) rather than Proven (green).
## Reading the Dependency Graph
In the dependency graph, node colors show you the health of your project at a glance:
- A graph that is mostly **dark green** means the formalization is nearly complete.
- Clusters of **orange** nodes indicate areas where formalization hasn't started.
- **Red** nodes are active work areas with incomplete proofs.
- **Purple** nodes are intentional axioms -- structural foundations, not gaps.
- Isolated **green** nodes surrounded by orange may indicate proofs that need their dependencies filled in before they can become fully proven.
- A disconnected subgraph (nodes not connected to the rest) is a warning sign -- it may indicate that "proven" results don't actually follow from the intended foundations.
## Priority Order
When multiple conditions apply, status is determined by this priority (highest first):
1. Mathlib Ready (manual)
2. WIP (manual)
3. Not Ready (manual, if explicitly set)
4. Fully Proven (automatic)
5. Axiom (automatic)
6. Sorry (automatic)
7. Proven (automatic)
8. Not Ready (default)