focs-experiments

FOCS Experiments

FOCS solicits research on the theory of computation; nothing in the 2026 CFP

asks for an evaluation, a benchmark, or an artifact (checked 2026-07-08).

Most accepted papers contain no computation at all, and a submission that

needs an empirical section to be persuasive is signaling that it belongs at

an algorithms-engineering venue. Yet computation does appear in strong FOCS

papers — inside proofs, behind constructions, and occasionally as a figure.

This skill scopes each mode so it helps rather than hurts.

Referee questions, by computational mode

The useful frame is not "may I include code?" but "what will a theory referee

ask about this computation?" — because each mode triggers a different

interrogation:

| Mode | Referee's question | Your obligation |

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

| Case analysis inside a proof (finitely many configurations checked by program) | "If this program is wrong, is the theorem false?" | Yes → full rigor: deterministic run, published certificate, an independent checker a reader can audit |

| Search that found an object (a gadget, a code, a hard instance) later verified by hand | "Is the object's correctness independent of how it was found?" | Verify the found object analytically or by a trivially-auditable checker; describe the search in one honest sentence |

| Numerical exploration that motivated a conjecture-turned-theorem | "Does the paper claim anything based on the numerics?" | No claims may rest on it; at most a remark crediting the exploration |

| Illustrative plot of the algorithm's behavior | "Is this decoration or evidence?" | Label as illustration, disclose instance generation and seeds, make no comparative-performance claim |

The forbidden mode is the missing row: runtime comparisons against prior

implementations. That evidence form has real homes — SODA's experimental

track culture, ALENEX, ESA — and importing it into a FOCS submission invites

the committee to judge the theorems as insufficient on their own.

Rigor pattern for a proof-bearing computation

When a lemma's truth rests on a machine check, engineer it like a proof step,

because it is one. The pattern that satisfies skeptical referees:

# Lemma 4.7: no 3-colorable configuration of size <= 11 exists.
# The enumerator is complex; the checker is small enough to audit.
verify: configs.enum
	python3 check_lemma47.py configs.enum   # 40 lines, stdlib only
	sha256sum -c configs.enum.sha256        # pin the enumerated set
configs.enum:
	./enumerate --exhaustive --size 11 > configs.enum

Three properties matter: the checker is short and transcribes a definition

from the paper verbatim; the enumerated evidence is content-addressed so a

re-run is comparable; and the paper's proof text says precisely what the

computation certifies ("the program verifies that each of the 2,146

configurations fails condition (ii) of Definition 4.5") rather than gesturing

at "extensive computer verification". Deposit the checker and the certificate

with the public full version (focs-artifact-evaluation).

Discovered objects, honestly credited

A construction found by simulated annealing, SAT solving, or an LLM-guided

search is fully legitimate at FOCS — the community judges the object, not the

finder. Honesty norms:

• Report the finder's nature truthfully; do not dress a heuristic search as

exhaustive, and do not claim exhaustiveness you cannot certify (a

nonexistence claim silently upgrades the computation to proof-bearing).

• If the object is small, print it in the paper; an explicit 40-entry table

beats "available in our repository" for a reviewer deciding correctness.

• The interesting open question "why does this object exist?" can be posed as

such — FOCS tolerates, even likes, a proof that works for reasons not yet

structurally understood, provided the paper says so.

Where the computation is described

Placement follows proof weight. A proof-bearing computation is described in

the proof itself — search space, what the output certifies, where the

certificate lives — because a proof with an undocumented machine step is

incomplete inside the ten-page window's promises (focs-writing-style). A

discovery gets one sentence at the construction's first appearance. An

illustration lives in a figure whose caption is self-sufficient. What never

works is a trailing "Implementation" section: it signals to a breadth

reviewer that the paper wants evaluation credit, and it buries proof-relevant

information where depth reviewers will not look for it.

Plots without performance theater

An illustration is admissible when it teaches, not when it argues. A figure

showing the recursion depth of your algorithm on random instances can make an

amortization argument vivid; the guardrails are a caption that names the

instance distribution and seed, axes that start at zero or say why not, and

no baseline curves — the presence of a competitor curve converts illustration

into benchmark and triggers the missing-row problem above.

Disclosure when the finder is an AI system

Search by LLM-guided methods is entering theory workflows, and the norms

above extend cleanly: the found object is still judged on its own

verification, and the finder is still reported honestly ("the candidate

inequality was proposed by an LLM-assisted search and verified in Lemma

5.2"). Two cautions specific to the current moment: check the live CFP for

any AI-use disclosure policy before submission (none appeared in the FOCS

2026 CFP at the 2026-07-08 check; future cycles 待核实), and never let

generated text stand in for a proof step — the verification obligations in

the table above attach to the claim, not to the tool that produced it.

Decision rule

If deleting every computational element leaves the paper's claims intact, the

elements are decoration: keep only those that teach. If deleting one makes a

theorem unproved, that element is a proof step: give it proof-grade rigor. If

deleting them makes the paper unconvincing, the paper is at the wrong venue —

return to focs-topic-selection and route toward the algorithms-engineering

ecosystem before investing in FOCS formatting.