Status Badge

The status badge

Every conjecture carries one badge showing how far it has got. Click any badge to come back here.

It is worked out from six fields on the conjecture’s own page, always the same way, never by hand, and it answers two questions: how solid is the statement, and how far has the proof got.

Those stay apart for a reason. A machine can verify a Lean proof and you can still have proved nothing about the conjecture, because the Lean might not say what the English says. So “somebody checked the Lean matches the English” is its own signal, not a footnote.

What the parts mean

Outer ring — how solid the statement is (a score called σ, 0 to 5)
Pale to strong green, lightest (0) to darkest (5). 0–1 = there is only an English statement. 2–3 = someone has written it in Lean, but nobody has checked the Lean says the same thing. 4–5 = written in Lean and checked to say the same thing
Dotted ring — written in Lean, but nobody has checked the Lean matches the English. This is the case to watch: proving the Lean version tells you nothing about the conjecture until someone confirms they are the same statement
Dashed ring — an AI checked that the Lean and the English say the same thing
Solid ring — a person checked that the Lean and the English say the same thing
Inner disc — how far the proof has got (a score called π, 0 to 4)
White (0, nobody has tried) through to strong green (4, checked by machine). A blank disc means no attempt at all, which is deliberately different from even the palest green. Levels 1 to 4 use the same green as the ring, so the badge just gets greener as a conjecture progresses, whichever half is moving
Centre mark — repeats the proof score as a symbol, so you do not need to see colour
– 0 — nobody has tried yet
· 1 — an AI wrote a draft; nobody else has checked it
• 2 — a person either wrote the draft or reviewed it, but not both
● 3 — a person wrote it and a person reviewed it, but it is not in Lean
✓ 4 — checked by machine: a finished Lean proof, with no sorry left standing in for a missing step. At this point it stops mattering who wrote it, because the proof checker is what decides
Seal
Thin gold halo — appears only when a person has confirmed the Lean matches the English (σ ≥ 4) and the proof is checked by machine (π = 4). This is the strongest state the badge can show: everything rests on a small proof checker rather than on anyone's word
Direction — whether the work proves the statement or disproves it (proof_direction, optional, proves unless set)
• Red scale — the work shows the statement is false. Same shape, same scores, same lightness at every step: a red badge is exactly as strong as the green one next to it. It is not a warning
✗ A cross instead of a tick at 4 — a machine has checked the disproof. The gold halo still applies, because it means the checking is complete, not that the statement is true

Direction is not a score. A badge can say the work disproves the statement, and that never changes either score: a machine-checked disproof is as finished as a machine-checked proof. You cannot claim one without a proof, either – proof_direction: refutes with the proof still open is rejected at build time.

If you cannot see the colours. At the top of the proof scale the cross works on its own. Lower down, colour is the only visual difference, so the caption and the screen-reader label say “Refutation” instead of “Proof”, and the one-line summary is expected to as well. Read those, not the hue.

The six fields

Statement half (outer ring): who wrote the English (statement_informal), whether it is in Lean and who put it there (statement_formal), and whether anyone checked the Lean matches, and who (statement_match). Score 0 (AI-written, not in Lean) to 5 (written, formalised and checked, all by people).

Proof half (inner disc): whether there is a written proof and who wrote it (proof_informal), whether anyone reviewed it (proof_review, which stops mattering once a machine has checked a proof), and whether there is a finished Lean proof (proof_formal – no sorry standing in for a missing step). Score 0 (nobody has tried) to 4 (machine-checked). At 4, who wrote it stops mattering: the proof checker decides.

Each score has a second channel so the badge survives black and white. The ring’s line style: dotted means nobody has checked the Lean against the English, dashed means an AI did, solid means a person did. The disc’s centre mark: – · • ● ✓. Everything turns red when the work disproves rather than proves, with ✗ at the top. A thin gold halo, the seal, appears only when a person confirmed the match and a machine checked the proof. Hover any badge for the full status in words.

Statement: AI-written, not yet formalized. Proof: open -- no attempt yet. – Nothing in Lean yet. This is where every new conjecture on this site starts
Statement: human-written, AI-formalized, not yet matched against the informal statement. Proof: AI draft, not yet independently reviewed, not yet formalized. · A machine wrote the Lean, but nobody has checked it matches the English. Do not read this as a verified statement
Statement: human-written, AI-formalized, AI-matched against the informal statement. Proof: human draft, human-reviewed, not yet formalized. ● An AI confirmed the Lean matches, and a person reviewed the written proof. Real progress, but no gold halo yet
Statement: human-written, human-formalized, human-matched against the informal statement. Proof: machine-checked (AI-formalized). ✓ A person confirmed the Lean matches and a machine checked the proof. Gold halo
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 disproof. It gets the gold halo too, because the halo is about the checking being complete, not about the answer

To change a status, edit the status.* fields in c/<id>/index.qmd and run python3 scripts/status_badge.py from the repository root. Never edit status_badge: by hand.

Difficulty

Every conjecture also carries a difficulty grade, an italic tag with the reason on hover.

It measures one thing: how far the conjecture is from techniques that already exist, or what a solution would have to invent. Not the effort, which depends on who is working. Not the chance of being solved by some date, which no honest grader could defend.

Effort is tracked separately, and only for a machine on a fixed budget: see attackability. It does not feed this grade, and the two disagree often.

Grade What it says
routine A standard technique works as it stands.
adaptation An existing technique has a visible route, with a real obstacle on it.
new-idea Nothing in the literature gets there. Something unpublished is needed.
barrier A published result says techniques of this kind cannot suffice.

Every grade records whether a person or a machine decided, and shows (ai) where a machine did. A machine may never mark its own work as a person’s. Where evidence is thin the grade rounds towards harder than it looks. Every grade needs a one-sentence reason, and the reason is the part worth checking, so a conjecture without one fails the build.

What the badge cannot tell you

The badge is a function of those six fields and nothing else, so it cannot call a result settled before a machine has checked it. Two things beside it fill the gap: the one-line summary (status_summary), required and shown in every listing table, and the category, without which a result that is proved but not yet in Lean would look identical to one nobody has touched. c/0004 is the example – informal proof, low badge, and the category and summary are what say so.

Each conjecture page also lists its open obligations: unverified steps, unaudited files, unmatched Lean statements, missing sanity checks. The open count is its own column in listing tables.