First, the venue truth: SODA has no artifact-evaluation track. Referees judge
proofs, not repositories. But two kinds of computational objects still matter to a
SODA author, and the co-located satellite ALENEX runs a genuine AE process — for
the 2027 cycle, ALENEX's dates were: submission July 20, 2026; notification early
September 2026; artifact submission September 11, 2026; AE rebuttal October 12-14;
AE results by October 16, 2026, with a dedicated HotCRP AE site
(alenex27ae.hotcrp.com; checked 2026-07-08 via search renderings of the SIAM
ALENEX27 pages).
| Situation | Artifact's role | Correct home |
|---|---|---|
| Proof relies on machine computation (case enumeration, SAT/ILP certificate, verified numerics) | Part of the proof — reviewers must be able to check it | The SODA submission itself, described in the paper, archive linked |
| Implementation exists but the claim is the theorem | Supporting color; zero review weight at SODA | arXiv full version appendix + repository; one paragraph in the paper |
| The experiments are the contribution (engineering, tuning, real datasets) | The reviewed object | ALENEX, with its AE process — not SODA |
The routing mistake costs a cycle: an implementation-led paper at SODA reads as a
theorem-light submission; a theorem-led paper at ALENEX reads as an experiment-light
one. soda-experiments covers the boundary in detail.
When a lemma's truth rests on computation, treat the computation like a proof step:
github.com/yourname defeats the author-block scrubbing.A minimal verification bundle that a skeptical theorist can run:
verification/
├── README.md # lemma ↔ computation map; expected output; runtime
├── generate.py # enumerates the finite case space (deterministic)
├── check.py # validates each case; exits nonzero on failure
├── certificates/ # per-case witnesses, checkable independently
└── environment.txt # exact toolchain versions
The README's first line should be the command that reproduces the check, and the paper should quote the total case count so a re-runner knows when they are done.
Choosing the certificate form is the design decision; everything else is plumbing. Patterns that referees can check without trusting your code:
| Claim shape | Certificate | Independent check |
|---|---|---|
| "No object with property P exists below size k" | Exhaustive enumeration transcript + case count stated in the paper | Re-run enumeration; compare count |
| "Formula/configuration is unsatisfiable" | DRAT or similar proof log from the solver | Standard proof checker, not your solver |
| "This LP/SDP bound holds" | Dual solution with rational entries | Verify feasibility + objective by exact arithmetic |
| "This extremal object exists" | The object itself, in a documented format | Verify its properties directly (cheap direction) |
| "Constant c < 1.4142" | Interval-arithmetic evaluation script | Re-run with a different interval library |
Two disciplines cut referee effort by an order of magnitude: make the checking program trivial even if the searching program was heroic, and put the case count / certificate size in the paper so a verifier knows what "done" looks like before starting.
If the artifact is the point, the ALENEX pipeline gives it real review: artifacts are submitted after paper notification (September 11, 2026 for the 2027 cycle), evaluated with a rebuttal round in mid-October, and the results feed the final paper. Practical notes for a SODA-adjacent group:
A theory referee meeting a machine-checked lemma asks three questions in order, and the paper should answer them in the same order: Is the reduction from lemma to finite check proved? (prose, in the paper, no code involved); Could the check be wrong? (certificates checkable by independent tools answer this; "our program says so" does not); Can I re-run it before my review is due? (state the runtime — an hour on a laptop invites verification, a week on a cluster invites suspicion). Papers that answer all three convert the computational step from a reviewing liability into a fully-verified component; papers that answer none of them get reviews containing the phrase "we were unable to verify," which at a proofs-are-the-product venue is close to fatal.
[Artifact routing] SODA-internal proof evidence / arXiv companion / ALENEX AE
[Proof-dependence audit] <claims whose truth relies on computation, and their certificates>
[Anonymity state] <archive hosting compatible with double-blind: yes/no>
[AE calendar] <applicable ALENEX dates, owner per deadline>
[Release plan] <post-acceptance versioning and DOI>