The Proof Manual

For agents: load proof-manual.yml.

You have a conjecture. You try induction. It doesn’t work. Now what?

Most people try induction again, harder. Schoenfeld (1985) filmed this: one technique, ridden to exhaustion, consuming the entire session. He called it the wild goose chase. Novices and experts know the same techniques. The difference is control — knowing when to switch and what to switch to.

He never specified what. This manual does. It doesn’t prove your theory right. It makes it faster for it to be wrong.

The procedure

1. Revalidate the problem’s status against dated primary sources. Repeat this before claiming novelty; “open” is not stable metadata.
2. Formalize the claim and its quantifier order. Decide what would count as a witness, bound, construction, or impossibility; then let later-bound objects depend adversarially on every earlier choice.
3. Decompose it into lemmas. Separate the structural problem from the local calculations.
4. Classify each lemma by claim and domain, then look up candidates in the grid. Scan the whole row, not just your first instinct.
5. Retrieve analogues. Look for the same shape in another theorem or domain.
6. Check kill conditions and symmetries. Cross off the dead techniques before you start.
7. Try the survivors in parallel when you can. Verify each step, not just the conclusion, and record the verification grade.
8. Diagnose the failures. Repair the statement, invent a missing lemma, change domains, or escalate to the technique the failure names.
9. Repeat until the proof closes or the conjecture breaks.

This is the proof loop:

status → formalize → decompose → retrieve → generate → search
  ↑                                                   ↓
  └────────── mutate ← diagnose ← verify ─────────────┘

A stale status check can waste the whole loop: a proof may have appeared after problem selection, or a newer theorem may make the chosen route obsolete. Record the query date, theorem statement, and primary source—not just “believed open.” Literature discovery is not a new proof, but failing to do it can turn genuine proof search into accidental reproduction.

Quantifier order deserves the same treatment. To test ((\exists D,\forall d\ge D,\forall v)), choose ((v)) after seeing ((d)); never test only a fixed collection of ((v)) while increasing the grid. Uniform discretization claims are especially vulnerable because the object can scale with the denominator and hide between every sampled point.

Carry theorem domains forward verbatim. A finite bound for counterexamples does not bound every object in a wider near-extremal band, even when every counterexample lies inside that band. Either retain the counterexample-only conclusion or derive a new bound for the wider antecedent.

Separate the strict interior from the boundary of every sharp threshold. Equality cases often carry rigid extremizers that weaken the structural statement even though a counterexample would satisfy a strict inequality. When the threshold is rational, normalize there before searching: exact boundary equations may expose the small integer labels the proof needs. Test <, =, and ≤ as different hypotheses, and use a rational grid only as a necessary filter until the intervals between grid points are controlled.

Quotient out invariances before stating an arithmetic hypothesis. If the target is unchanged by common dilation but “some coordinate is divisible by (m)” is not, divisibility is meaningful only for the primitive representative. Testing millions of primitive examples does not validate a theorem whose written quantifier still includes their dilations.

Then audit the conclusion for operational content. “There exists a relation permitting descent” is not a lemma until the permitted transformation and its preserved invariant are stated. If the bare relation exists for every object in the domain, the adjective is carrying the entire proof and the hypothesis cannot yet be tested.

Audit composition too. Two unrelated certificates can be added into one artifact whose support appears to bridge both components. Before treating support as connectivity, factor out disjoint subcertificates or measure an invariant such as rank that cannot increase under cosmetic recombination.

When bounded relations reach full rank, take cofactors immediately. A primitive one-dimensional kernel is generated by the maximal minors, so Hadamard converts coefficient bounds into an explicit height bound. State what remains after that reduction: a smaller finite search is useful, but it is not a uniform proof.

When a covering argument stalls at a loose union bound, classify the witnesses before estimating the sets again. A witness that only one class of set can cover creates an exclusive obligation; incompatible obligations require distinct sets. Prove the resulting lower bound is exact by constructing a cover from those classes. This can expose the adversarial equality pattern that a full proof must handle, whereas another capacity estimate only repeats the original information loss.

If the witnesses carry nonnegative weights, normalize the total simultaneous slack by the sum of the leave-one-witness-out slacks. This deletion ratio measures the correlation tax directly: independence usually gives reciprocal scale, while structural relations are the only way an adversary can drive it lower. State that dependency budget explicitly—rank, dimension, or circuit count—and test a quantitative floor conditional on it. The resulting inequality may survive even when every greedy load-allocation rule fails.

For continuous window covers, ask whether feasibility is witnessed at an entry or exit event. Prove that reduction topologically—a nonempty proper closed feasible component has a boundary—before replacing the continuum by endpoints. Then count event ownership, not just interval measure. If raw capacities still cover the demand, measure duplicated ownership with intersection moments; odd Bonferroni truncations give certified upper bounds, while an unproved low-order truncation is only a hypothesis.

Near a sharp packing threshold, compare two packings that share all but one piece. Remove the common pieces and measure the total complementary slack. If that slack is smaller than one piece, there is only one complementary component large enough to hold either replacement; both replacements must occupy it, so the distance between them is at most the total slack. This converts a global measure deficit into a sharp positional bound without estimating every gap separately.

Repeated overlap support need not imply a relation among the participants. Preserve the event coordinates and signed residuals before compressing a congested cluster. Subtracting two occurrences can cancel a shared affine phase and turn repeated overlap into a difference-set or lattice statement; discarding the coordinates first destroys that invariant.

When borrowing from another field, transfer the proof decomposition before transferring any theorem. A useful analogue may suggest a dichotomy—recursively remove a locally reducible object, or classify the rigid core left behind—even when its domain-specific conclusion is irrelevant. Restate each branch in the target object’s invariants and prove it there. Shared vocabulary such as “coverage,” “time,” or “load” is evidence for an experiment, not permission to import a lemma.

When adversarial groups are iterates of one transformation, search its fixed and short-period points before scheduling the groups independently. A fixed point can collapse many apparent time scales to one phase, turning a mixed case back into a solved base block. Then discard the construction syntax and identify the actual invariant—often a shared residue palette or quotient action—which may certify many unrelated-looking objects. For unequal groups, write the safe phase interval first and ask whether the fixed-point grid intersects it. Record both the exact grid criterion and a coarse scale at which intersection is automatic; otherwise “synchronization” is only a metaphor.

If one group is bad on an entire candidate grid, solve that group in the quotient first and use its feasible phase as a common offset. Then sweep the remaining grid symmetry and charge each outside constraint only for the classes it blocks. This turns a fatal zero residue into a lower-dimensional subproblem plus a finite load bound.

Separate certificate existence from certificate selection. A sweep, greedy order, or geometric pivot may repeatedly find the witnesses you need and still fail on an example where the full witness family proves the theorem. When a selection rule breaks, compute an order-independent invariant—such as the rank or span of every valid certificate—before weakening the conclusion. The failed algorithm may diagnose its own locality, not a mathematical obstruction.

Audit computation against the theorem lattice. An exhaustive classification may be correct yet logically redundant because an older extremal theorem already gives a stronger bound on the entire domain. Run the computation as an independent audit if it is useful, but move the theorem—not the table—into the proof’s load-bearing path.

The techniques are old. What changed is how quickly a mathematician—or an agent—can generate, reject, repair, and recombine them. Control is no longer just knowing what to try next. It is managing the loop.

Verification has levels

“The solver says UNSAT” is not the same result as a proof a stranger can check.

Verification also perturbs the search. Proof logging, named clauses, and assumption tracking can make a terminating solve time out. That timeout is not evidence against the claim; it is an instrumentation failure. Record it as unknown, then change the verifier or reduce the instance. Never compress unknown into false.

A certificate verifies the formula it receives, including any symmetry breaks, cuts, or derived clauses—not the claim that those strengthenings are sound. Record a proof that each added constraint preserves every hypothetical counterexample. Otherwise a perfectly checked UNSAT result may certify only an accidentally stronger problem.

Kill conditions

The part nobody writes down.

The kill at step N names the technique at step N+1.

Preserve maneuvering room

An inductive witness is often stronger than the larger problem needs. Freezing it at its exact optimum can destroy every extension even when a nearby, slightly weaker witness extends cleanly. Treat the surplus as a routing budget: identify the connected feasible component, move inside it, and update the remaining constraints only when a boundary event occurs.

This is the proof analogue of an augmenting-path algorithm. The invariant is not “keep the partial solution optimal.” It is “keep it feasible above the threshold while searching for a free slot.” Test the frozen optimum first; if it fails, lower it only to the strongest scale justified by the final theorem.

A conserved deficit is bookkeeping, not termination. Once it identifies the legal handoffs, look for the timestamp, ordering, or boundary condition that makes some refinement monotone; otherwise the same finite load may circulate.

Symmetry mismatch

If your problem lacks a symmetry your technique assumes, the technique produces a valid-looking argument with a hidden gap.

Embed-solve-pullback

When nothing in your domain works, change the domain.

The risk is always the same: the pullback doesn’t preserve the constraints.

The lineage

Every technique exists because its parent died on a specific problem:

Exhaustion (Archimedes)
  kill: can't handle infinite processes
  └→ Limits (Cauchy, Weierstrass)
     kill: need compactness for existence
     └→ Compactness arguments (Bolzano-Weierstrass)
        kill: need topology beyond R^n
        └→ General topology

Counting (Euler)
  kill: exact counts intractable
  └→ Generating functions
     kill: coefficients hard to extract
     └→ Analytic combinatorics (Flajolet)
        kill: need asymptotics not exact
        └→ Probabilistic method (Erdős, Alon & Spencer)

Diagonalization (Cantor)
  kill: need self-reference formalized
  └→ Incompleteness (Gödel)
     kill: need computation model
     └→ Undecidability (Turing)
        kill: need quantitative hardness
        └→ Complexity lower bounds (Cook, Karp)

A student who only knows induction will never try a potential method. One who knows potential methods exist because induction kills residual structure will reach for the right tool.

Why it works

Every proof decomposes into compositions of six type constructors:

The grid’s rows map to these: existence = Σ, impossibility = Π→False, construction = Σ with computability. This explains the target shape, but not the whole search. A failed proof may be a type error; it may also be a missing lemma, an unproductive decomposition, a bad formalization, or a search budget spent in the wrong branch. Lean can reject an invalid proof term. It cannot tell you whether you stated the right theorem or searched the right neighborhood.

That distinction matters more now that proof generation is abundant. Verification answers is this derivation valid? The manual answers what should we try, what did the failure teach us, and how should we change the search?

Pick your stuck conjecture. Run the procedure. If the manual doesn’t surface a technique you haven’t tried, it’s incomplete — tell me what’s missing.

Inspired by The Parts Bin.