Status Badge Legend

The status badge

Each conjecture carries one badge summarizing where it stands. It’s a deterministic function of six graded fields tracked in the page’s status: frontmatter, plus one optional field saying which way the work points — never hand-picked. A machine-checked proof of an unmatched formalization certifies nothing about the conjecture itself, so the badge treats whether the formal statement actually matches the informal one as a first-class signal, not an afterthought. Click any badge, anywhere on the site, to come back to this legend.

Symbol key

Outer ring — statement grade σ (0–5)
Pale → saturated green, lightest (0) to darkest (5): 0–1 = only an informal statement exists; 2–3 = formalized in Lean but not yet matched against the informal statement; 4–5 = formalized and matched
Dotted ring — formalized, but not yet matched against the informal statement (the dangerous cell: a proof about this statement proves nothing about the conjecture until it's matched)
Dashed ring — an AI checked the formalization matches the informal statement
Solid ring — a human checked the formalization matches the informal statement
Inner disc — proof grade π (0–4)
White (0, nothing attempted) → saturated green (4, machine-checked): a blank disc means no proof attempt at all, distinct from even the palest green. Levels 1–4 use the same green as the ring — the whole badge reads "more green" as a conjecture progresses, regardless of which side is moving
Centre glyph — restates the proof grade π as text, independent of colour
– π = 0 — no proof attempt yet
· π = 1 — AI draft, not yet independently reviewed
• π = 2 — one of {draft author, reviewer} is human
● π = 3 — human draft, human-reviewed, still not formalized
✓ π = 4 — machine-checked (a completed Lean proof, not just a sorry); who wrote it no longer matters, the kernel is the arbiter
Seal
Thin gold outer halo — appears only when σ ≥ 4 (human-matched) and π = 4 (machine-checked): the fully de‑Bruijn‑verified state
Direction — which way the work points (proof_direction, optional, default proves)
• Red ramp — the work refutes the statement rather than proving it. Same geometry, same grades, same lightness at every step: a red badge is exactly as strong as the green one beside it, not a warning
✗ π = 4 with a cross instead of a tick — a machine-checked refutation. The seal still applies: it means de‑Bruijn‑complete, not "true"

Direction is not a grade. It never enters σ or π, and it cannot: how well established a result is and which way it points are different questions, and a machine-checked refutation is exactly as finished a piece of work as a machine-checked proof. A refutation also requires an actual proof of one — proof_direction: refutes with proof_informal: open is rejected by the build, since nothing is refuted by the mere suspicion that it is false.

Where colour is the only channel, and what to do about it. Red and green are the classic colour-blind pair. At π = 4 the cross carries the direction on its own, so the badge survives greyscale. At π = 1–3 — a refutation drafted but not yet formalized — colour is genuinely the only visual channel, and the honest fix is that it is not the only channel: the badge’s caption and its aria-label both say “Refutation” in place of “Proof”, and status_summary is expected to say so in words too. Read those, not the hue, if the hue is not available to you.

Statement side (outer ring): statement_informal (ai/human — who wrote the informal write-up), statement_formal (open/ai/human — has it been formalized in Lean, and by whom), statement_match (open/ai/human — has that formalization been checked against the informal statement, and by whom). These combine into a statement grade σ from 0 (AI-written, unformalized) to 5 (human-written, human-formalized, human-matched).

Proof side (inner disc): proof_informal (open/ai/human), proof_review (ai/human — vacuous once a formal proof exists), proof_formal (open/ai/human — a completed Lean proof, not just a sorry). These combine into a proof grade π from 0 (no attempt) to 4 (machine-checked — once a proof is formally verified, the Lean kernel is the arbiter, so who wrote it no longer affects the grade, only a caption detail).

Reading the badge: the outer ring’s colour is the statement grade; its line style is the match status redundantly (dotted = unmatched, dashed = AI-matched, solid = human-matched) so it survives greyscale. The inner disc’s colour is the proof grade, with a centre glyph (– · • ● ✓) as a second redundant channel. The whole ramp turns red, at matched lightness, when the work refutes the statement instead of proving it, and the π = 4 glyph becomes ✗. A thin gold outer halo (a seal) appears only when the statement is human-matched and the proof — or the refutation — is machine-checked, the fully de-Bruijn-verified state. Hovering any badge shows the full plain-English status as a tooltip.

Five examples, from nothing-done to fully sealed, the last two in each direction:

Statement: AI-written, not yet formalized. Proof: open -- no attempt yet. – Nothing formalized yet (today's default for every new conjecture on this site)
Statement: human-written, AI-formalized, not yet matched against the informal statement. Proof: AI draft, not yet independently reviewed, not yet formalized. · Statement autoformalized but unmatched — the dangerous cell: don't mistake this for a verified statement
Statement: human-written, AI-formalized, AI-matched against the informal statement. Proof: human draft, human-reviewed, not yet formalized. ● AI-checked match, human-reviewed informal proof — real progress, still not sealed
Statement: human-written, human-formalized, human-matched against the informal statement. Proof: machine-checked (AI-formalized). ✓ Human-matched statement, machine-checked proof — sealed
Statement: human-written, human-formalized, human-matched against the informal statement. Refutation: machine-checked (AI-formalized). ✗ The same state, pointing the other way: the statement is false and a machine has checked the refutation — also sealed, because sealed means de‑Bruijn‑complete

To update a statement’s status: edit the status.* fields in its c/<id>/index.qmd frontmatter (the six graded ones, plus proof_direction if the work refutes rather than proves), then run python3 scripts/status_badge.py from the repo root to regenerate the badge (status_badge: in the frontmatter, and the inline copy between the <!-- status:start --> / <!-- status:end --> markers in the body); never hand-edit status_badge: itself.

Difficulty

Every statement also carries a difficulty grade, shown as an italic tag beside its other tags, with the reason on hover.

What it measures is one thing and not three. It is the distance from known technique: what a resolution would have to invent. It is deliberately not the expected effort, which depends on who is working and with what compute, and deliberately not a probability of resolution by some date, which eight statements cannot calibrate and which no honest grader could defend. Reading it as either of those will mislead you.

Grade What it says
routine A standard technique applies as it stands.
adaptation An existing technique has a visible route, with a real obstacle on it.
new-idea Nothing in the literature reaches the statement. Something not yet published is needed.
barrier A published barrier says techniques of the current kind cannot suffice.

Who graded it, and how to read that. Every grade carries ai or human, and the tag says (ai) where a model made the call. As everywhere on this site, a machine may never mark its own work as human, and a human assessment supersedes rather than silently overwrites. Where the evidence is thin the grade rounds towards harder than it looks, on the same principle as the badge: a grade may understate what is known, never overstate it.

Every grade carries a one-sentence reason, and the reason is the part to check. A grade you cannot argue with is not evidence, it is decoration, so difficulty.note is required and a statement without one fails the build.

Where the badge appears

The same single badge (ring and disc together) appears everywhere: in listing tables, and at the top of a statement’s own page, right before the Statement/Proof/Formal Artifact tabs.

Beyond the badge

The badge is deliberately narrow: it’s a pure function of the fields above, and always will be. It can’t say a result is actually settled before it’s machine-checked, and its own caption is necessarily brief. Two things next to it cover the rest:

status_summary, one required sentence, shown next to the badge in every listing table, so a facet page is scannable without opening every statement.

category matters here too: research-solved and test statements exist on the site precisely because the badge alone would make a proven-but-unformalized result look identical to an untouched one. c/0004 is a real example: proven informally, badge still low, category: research-solved and its status_summary are what actually say so.

Each statement page also has an ## Open obligations list: the concrete outstanding items (unverified steps, unaudited files, unmatched formalizations, missing sanity lemmas). The open count is its own column in listing tables.

In short: the badge and its caption summarize; status_summary and category say what the badge can’t.