focs-reproducibility

FOCS Reproducibility

FOCS has no reproducibility checklist and asks for no artifacts (2026 CFP,

checked 2026-07-08). At a proofs venue, "reproducing" a result means an

independent expert can re-derive it from the paper alone. That property —

checkability — is engineerable, and papers engineered for it survive both

refereeing and the decade of scrutiny that follows a FOCS acceptance. Four

practices below build it.

1. The hypothesis ledger

Every assumption a theorem consumes should be visible at the theorem, not

scattered across ambient conventions declared in Section 2. Keep a ledger

during writing:

| Hypothesis | Introduced | Used by | Discharged or standing? |

|---|---|---|---|

| $G$ simple, connected | §2 conventions | Thm 1, 3; Lem 4.2 | standing |

| $\varepsilon < 1/\log n$ | Thm 3 statement | Lem 5.1–5.4 | standing — stated in Thm 3 ✓ |

| oracle access to exact eigenvalues | §5 ¶1 (silent!) | Lem 5.3 | must surface in Thm 3 |

The audit question for each row: does the formal statement of every theorem

that transitively needs this hypothesis mention it? Silent standing hypotheses

are the most common correctness complaint theory referees file, and the

cheapest to fix before submission.

2. Statement freeze across versions

A FOCS project lives as at least three documents — the HotCRP submission, the

arXiv/ECCC full version, and eventually the IEEE proceedings version. Theorem

statements must be bit-identical across them; a bound that strengthens

silently between submission and arXiv is, to a referee who checks, either

sloppiness or misconduct. Enforce the freeze mechanically by extracting and

diffing labeled statements:

# extract_statements.sh — run against any two versions of the source
for src in "$1" "$2"; do
  awk '/\\begin{(theorem|lemma|corollary)/,/\\end{(theorem|lemma|corollary)/' \
      "$src"/*.tex | tr -d ' \n' | sha256sum
done
# identical hashes => no drift in any formal statement

Legitimate post-submission improvements go into a dated "changes since

submission" note in the arXiv version, never into silent edits (see

focs-camera-ready for the endgame version ledger).

3. The imported-theorem audit

Most FOCS proofs stand on external results, and the failure mode is citing a

theorem for slightly more than it says. Before the freeze, audit every import:

• Locate the exact statement in the cited source — theorem number, page,

and version (arXiv preprints renumber theorems between versions; pin the

version, per focs-related-work).

• Transcribe its hypotheses into your ledger and check your invocation

supplies all of them. The classic bug: importing a bound proved for

constant-degree instances into an unbounded-degree argument.

• Check parameter regimes. "For sufficiently large $n$" in the source must

be compatible with the $n$ your recursion actually feeds it.

• If the imported proof is folklore or unpublished, prove it in your appendix;

"well known" is not a citation a referee can check.

4. Certificates for computed steps

When a proof step is a computation (focs-experiments), checkability means a

stranger can re-verify without trusting your code: publish the certificate

(the enumerated cases, the SAT solver's proof trace, the exact rational

arithmetic transcript), ship a minimal independent checker, pin both with

hashes, and state in the proof what object certifies what claim. A referee

who can re-run a 40-line checker in a minute treats the step as proved; one

who is asked to trust an opaque 4,000-line search does not.

5. Errata as a first-class object

Checkability extends past acceptance. FOCS papers are cited for decades, and

the community's memory of an error is shaped by how it was handled:

• Maintain the changelog in the arXiv version as the single erratum channel;

a correction buried in a later paper's footnote does not reach readers of

the original.

• Downgrade honestly: if a repaired lemma now yields a weaker bound, the

changelog and the abstract both change — leaving a stale headline bound on

a corrected paper is the reputational worst case.

• Notify identifiable downstream users directly when a result they built on

moves; theory's dependency graph is small enough that this is feasible and

expected.

Pre-freeze checkability review

Run as a dedicated pass, separate from proofreading:

1. Ledger complete; no silent standing hypotheses (§1).
2. Statement hashes identical between submission source and full-version

source (§2).

1. Every external import located, transcribed, regime-checked (§3).
2. Every computed step certified and independently checkable (§4).
3. One non-author has re-derived the most delicate lemma from the paper text

alone — the strongest single predictor that referees will succeed too.

A paper passing all five is not guaranteed acceptance; it is guaranteed not

to be rejected for the reasons authors most regret, and it is camera-ready

for the public record that FOCS culture expects the full version to become.