Requesting a same-owner model-identity consolidation under the State alias system described in docs/site-data-v2.md ("Credit and ordering") and the projection-v4 notes in the README.
Owner: mlgraham (this account — all affected results live in results/mlgraham.json in leanprover/lean-eval-submissions)
Declared labels to consolidate (verbatim, as recorded in the results store):
github.com/mlgraham (Claude Fable 5) — 16 solvesgithub.com/mlgraham — public accepted source, packaged (Claude Fable 5) — 1 solvegithub.com/mlgraham (various models) — 31 solves
Requested canonical identity: github.com/mlgraham (various models) (label 3).
Context: the early solves were declared under label 1 before I settled on the consolidated label 3 for all later submissions. I then attempted to self-serve the relabel by re-submitting identical source trees under label 3 (lean-eval-submissions #1493, #1494, #1495). I understand now from the site docs that this was the wrong mechanism: the duplicate rows resolve to a second fallback identity rather than moving credit, so problems such as dimitrov currently show two credit identities for what is one submitter — which removes the unique-solve credit instead of consolidating it.
Under the documented rule ("Multiple base results that resolve to the same (canonical identity, problem) retain their individual problem-page records but contribute one standings solve", with acceptance order preserved), a reviewed alias for the three labels above to one canonical identity should merge these cleanly, with first-solve order carried by the original acceptance timestamps.
Happy to verify ownership in whatever form is useful, and to have the duplicate rows handled however is cleanest on your side. If this request belongs on Zulip or in a different repo instead, a pointer is appreciated.
Requesting a same-owner model-identity consolidation under the State alias system described in
docs/site-data-v2.md("Credit and ordering") and the projection-v4 notes in the README.Owner:
mlgraham(this account — all affected results live inresults/mlgraham.jsonin leanprover/lean-eval-submissions)Declared labels to consolidate (verbatim, as recorded in the results store):
github.com/mlgraham (Claude Fable 5)— 16 solvesgithub.com/mlgraham — public accepted source, packaged (Claude Fable 5)— 1 solvegithub.com/mlgraham (various models)— 31 solvesRequested canonical identity:
github.com/mlgraham (various models)(label 3).Context: the early solves were declared under label 1 before I settled on the consolidated label 3 for all later submissions. I then attempted to self-serve the relabel by re-submitting identical source trees under label 3 (lean-eval-submissions #1493, #1494, #1495). I understand now from the site docs that this was the wrong mechanism: the duplicate rows resolve to a second fallback identity rather than moving credit, so problems such as
dimitrovcurrently show two credit identities for what is one submitter — which removes the unique-solve credit instead of consolidating it.Under the documented rule ("Multiple base results that resolve to the same (canonical identity, problem) retain their individual problem-page records but contribute one standings solve", with acceptance order preserved), a reviewed alias for the three labels above to one canonical identity should merge these cleanly, with first-solve order carried by the original acceptance timestamps.
Happy to verify ownership in whatever form is useful, and to have the duplicate rows handled however is cleanest on your side. If this request belongs on Zulip or in a different repo instead, a pointer is appreciated.