# The fleet

Six adversarial roles, run locally before you pose. Each has a **win condition** and a **gate**:
what happens to the pose if it wins.

## Why roles and not replicas

Attackers have crisp win conditions and reviewers do not. "Review this statement" produces prose
that is impossible to act on and impossible to falsify. "Produce an artifact that passes this
verifier while proving nothing" produces either a file or a silence, and both are informative: the
file is a bug report, the silence is weak evidence that the cheap attacks are closed.

Replication does not buy this. Five agents of the same family reading the same paper agree because
they share a prior, and their agreement is a property of the training data.

---

## Role 1: Writer

**Input:** the full paper. **Wins by** producing a declaration that compiles and reads back to the
informal statement term by term: what is quantified, over what type, with which hypotheses, and
whether the conclusion is the strong or the weak form.

**Deliverable:** the Lean source (`root.formal` plus the canonical `Statements/<label>.lean`), a
line-by-line mapping from the informal sentence to the formal one, and the exact source locator it
came from. This role produces the draft; every other role attacks it.

---

## Role 2: Degenerate-artifact hunter

**Input:** the formal statement and verifier config only — deliberately not the paper, because a
submitter attacking your problem next year will not have it either.

**Wins by** any artifact that goes green and carries no mathematical content.

**Gate: if it wins, the verifier is broken. Do not pose.** Restate, and rerun the whole fleet.

### The catalogue

Work through all of it. Each entry is a real thing that typechecks.

| Attack | Shape | Why it passes |
|---|---|---|
| Vacuous hypothesis | `∀ x, False → P x` | `absurd`/`elim` closes it in one line |
| Unsatisfiable conjunction | `∀ n, n > 5 → n < 3 → P n` | same, dressed up |
| Empty quantification | `∀ x : Empty, P x` | no cases |
| Empty index set | `∀ i ∈ (∅ : Finset ι), P i` | `simp` |
| Degenerate instance | statement over a type with one inhabitant | `Subsingleton` collapses it |
| Trivially satisfied bound | `card G ≤ card G` after a mis-transcribed product | true, empty |
| Existential with a free trivial witness | `∃ x, x = x` hiding inside the real claim | `rfl` |
| Weakened hypothesis | the real theorem plus an extra hypothesis that never fires | the restatement attack |
| Strengthened conclusion that is actually weaker | swapped `≤` direction, or `∀`/`∃` order flipped | reads right, proves the easy side |
| Definitional escape | a commons definition that unfolds to `True` | the statement mentions it and means nothing |
| Zero/one boundary | the claim holds only at `n = 0`, and `n` is implicitly bound | typechecks, says nothing |

The repo ships a live specimen: `Submissions/S001/MalloryWeakened.lean` proves `∀ n, Even n → Even
(n * (n+1))` against a canonical `∀ n, Even (n * (n+1))`. It compiles, it is true, it has a real
proof, and it is not the theorem that was asked; only the anti-restatement check catches it. Read
it before you start.

**Also attack the checker** on a certificate problem: an unexpected encoding, an empty witness, a
witness that crashes it. A crash is `checker_error`, which is red; a crash *caught* and reported
`ok: true` is a green for nothing.

---

## Role 3: Negation prover

**Input:** the formal statement only. **Wins by** any artifact proving `¬ statement` (or a form
the bridge accepts) that grades green.

**Gate: if it wins, stop.** Either the statement is inconsistent as written or the bridge is not
pinned to the canonical type. Both are fatal and neither is fixable by adjusting config.

Cheap to run, and it catches a specific common failure: a quantifier order or negation scope that
makes the statement provably false, which then goes green because the verifier only asks whether
the submitted declaration inhabits the canonical type — and the canonical type is the wrong one.
A partial win is informative too: a negation proved on a natural sub-case means your statement is
over-strong and the scope string must say so.

---

## Role 4: Vacuity witness

**Input:** a worked example from the paper, or its smallest case. **Wins by** exhibiting a
concrete object satisfying every hypothesis, ideally as a Lean term that typechecks against them.

**Gate: if it cannot**, the hypotheses may be unsatisfiable and the theorem vacuous. Do not pose
without either the witness or an explicit note in `root.scope` saying satisfiability is open —
itself a legitimate thing to pose, if you say so.

The cheapest insurance in the fleet: a vacuously true theorem passes all five verifier checks,
because it is a genuine proof of a genuine proposition that happens to be about nothing. Giving
this role the paper's worked example is deliberate — if the statement is right, that example **is**
a witness and the job reduces to formalising it; if it is not, the formalisation is wrong and you
have found the error from a direction the writer could not.

---

## Role 5: Prior-art hunter

**Input:** a downstream citing paper's restatement, not the original, because how the field uses a
result is often not how the original states it.

**Wins by** a citation list where every entry carries `opened: true` and a one-line note on what
was actually in it. Then **fetch every item listed**.

**Gate: any `opened: false` on a `source`-role citation is a visible gap.** Carry it into the
`citations` array rather than deleting the entry, so reviewers see what was guessed at.

Not hypothetical: in the FGK campaign a run claimed the field's framework could not see
multiplicity multisets, and the claim died because Akman–Sissokho, *Canad. Math. Bull.* 68 (2025),
open access and one fetch away, builds its framework on exactly that type. A listed-but-unopened
citation is a prediction about a document, not a citation.

Also instruct this role to hunt **method ceilings**: barrier theorems, integrality gaps, proven
limitations of a relaxation, exhaustive computational negatives over a stated family. Nobody finds
these by accident and they are the most valuable entries in a `squeeze` space.

---

## Role 6: Differential implementer

**Input:** the same source text as the writer, a different model and harness where available.
**Wins by** finding an input where the two implementations disagree, having written the checker
(certificate problems) or the formal statement (Lean problems) independently, without seeing the
writer's output.

**Gate: any disagreement is a bug in one of the two.** Find out which before posing. Do not
average them, do not pick the prettier one, do not ship both.

For a Lean statement, "diff" means: does `example : A := @b` elaborate in both directions between
the two candidate canonical types? If so they are definitionally equal; if not, one of them is not
the theorem. For a certificate checker: run both over the same witness corpus, including role 2's
adversarial witnesses, and compare `ok` and `canonical` on every input. Differing `canonical`
values are as serious as differing `ok` values, because `canonical` becomes
`elaborated_term_hash` and decides what counts as a duplicate submission.

---

## Decorrelating the inputs

Diversity of **input** and **role** beats diversity of count.

**Vendor / model.** Use different vendors where available. Where they are not, vary harness and
prompt framing, and **say in the report that vendor diversity was unavailable** rather than
implying it was there: an overstated fleet is worse than a small honest one, because it is read as
independent confirmation.

**Source text.** Always vary this. It is free, and it is the axis that catches misreadings.

| Role | Source text |
|---|---|
| Writer | the full paper |
| Degenerate-artifact hunter | the formal statement and verifier config only |
| Negation prover | the formal statement only |
| Vacuity witness | a worked example, or the paper's smallest case |
| Prior-art hunter | a downstream citing paper's restatement |
| Differential implementer | the same source as the writer, different model |

Convergence from **different starting texts** is evidence. Convergence from the same text is one
opinion sampled repeatedly, and it will feel exactly as convincing.

---

## Running the fleet

Dispatch roles that touch disjoint files in parallel, in a single message. Roles 2, 3 and 4 all
write Lean into the same submission tree, so give them separate directories or sequence them.

Sequence dependent work from the calling thread: a subagent that ends its turn is finished and
never resumes, so "wait for the build, then commit" silently drops the commit. If a role must
block on a build, it blocks in the foreground and sees the result in the same turn.

## The fleet report

One page, in the pose report:

- for each of the six roles: model, source text, win/no-win, artefact path
- every attack from the degenerate catalogue that was tried, and its outcome
- the vacuity witness itself, or the explicit note that goes in `scope`
- every citation with `opened: false`
- any method ceiling found, with the citation that supports it
- whether vendor diversity was available, stated plainly

A no-win with no evidence of the attempt is not a no-win; it is a missing role.