Investigate: are all solved problems attributed on leaderboard, proof graph?

[cgbarlow]

Reconcile whether all solved problems are reflected on the leaderboard and proof graphs. I have a feeling that we've done more than we are seeing but I need you to check.

[cgbarlow]

Reconciliation: solved problems vs leaderboard & proof graph

Checked, with the numbers probed directly from the records rather than inferred. You were right — but only the proof graph was hiding work, not the leaderboard.

Ground truth (from the AISP records on main)

762 goals = 327 open · 3 blocked · 10 translated · 284 proved · 138 archived
424 verified proof records = 286 active (library/index) + 138 archived (packages/unsorry-archive-*/library/index)

1. Leaderboard — ✅ correct and in sync

python3 -m tools.leaderboard --check . is green. It counts all 424 verified proofs, including the 138 archived ones — the generator explicitly globs packages/unsorry-archive-*/library/index/ and remaps archive paths back to canonical form for git attribution. The committed docs/leaderboard.* and docs/metrics/*.json match a fresh regen exactly. No undercount here.

2. Proof graph — ❌ the SVG was badly stale (this is the "more than we're seeing")

• docs/proof-graph.svg (the rendered preview / README card) showed 153 goals · 104 proved.
• A fresh regen shows 762 goals · 284 proved.
• The graph image was under-counting proved goals by 180 — frozen at an old snapshot.

Root cause: proofs-visualisation.yml regenerates all three outputs (--write) but its commit $paths list omitted docs/proof-graph.svg, and its drift gate git diff --quiet -- $paths only looked at the .md/.html. So the bot regenerated the SVG every run but never staged it, and reported "already in sync" — the SVG could never be pushed. Same path-gap class as the recent sourcing-leaderboard refresh fix. (The .md table and .html page were current — 284 proved · 138 archived — because they're in $paths; only the SVG drifted.)

Fix: #1899 — adds docs/proof-graph.svg to the tracked $paths and regenerates it so main reflects reality now. tools.visualiser --check . is green after.

3. Attribution gaps — counted, but not all credited to a name

Of the 424 verified proofs, 273 have no explicit solver≜ field; they're attributed by git add-author. All 273 are git-mappable (attribution-gaps.json: unmapped_missing_solver: 0), but many resolve to historical/unknown identities, so the board credits 151 to named contributors and buckets 273 as "historical/unknown". The proofs are counted — they're just not all attached to a contributor row. This is already tracked by docs/metrics/attribution-gaps.json (in sync). Closing it further is an aliasing effort (extend contributor-aliases.json), separate from this issue.

4. Two genuinely-proved goals shown as unsolved (minor data-integrity)

Each has a verified proof index record but a goal status that was never flipped to proved:

• no-nat-sq-eq-two-mul-sq-s4 → status≜open, sha≜∅ (proof 15cc9ae6…, positive_half_lt_of_even_nat)
• nat-zero-lt-succ → status≜translated, lean≜∅ (proof 4c71a8b4…, nat_zero_lt_succ)

They're inside the 424 verified count but appear open/translated on the queue/graph. I left the goal records alone (status transitions belong to the prove check-in flow under ADR-018, and this is 2 edge-case goals) — flagging for your call.

Bottom line

• Leaderboard: accurate, archived proofs included. No action needed.
• Proof graph: was showing 104/153 instead of 284/762 — fixed in fix: stage proof-graph.svg in the visualisation refresh (#1888) #1899.
• 273 proofs are counted but credited as historical/unknown (tracked, separate aliasing work).
• 2 proved goals mis-statused as open/translated (flagged).

[cgbarlow]

we need an automated process to work out who the 273 phantom solvers are