Proof complexity studies the resources needed to prove mathematical statements in precisely specified proof systems. In its central propositional setting, it asks how large a proof must be, how much information must be kept while producing it, and how difficult a suitable proof is to find. A statement can have an easily checked proof even when discovering that proof is difficult; a short informal explanation can also expand into a long derivation under restricted rules.
The gold standard is to name the statement, encoding, inference rules and resource measure before calling a proof efficient or a problem hard. This guide builds that discipline through complete resolution examples, explicit counts, a small allocation contradiction and changed-constraint exercises. The examples are original teaching constructions, not performance claims about a commercial solver or certificates for an actual engineering system.
Use the Gold Standard collection and How X Works hub for the wider subject map. Proof Theory explains inference and proof transformation; this guide concentrates on their computational cost. The Education guide supplies the learning test: can you preserve the reasoning when a rule, representation or assumption changes?
Choose your proof complexity route
Chapters 1–3: Read statements and inference rules
Chapters 4–6: Construct and measure proofs
Chapters 7–9: Compare resources and systems
Chapters 10–12: Connect evidence and applications
Chapter index
Read statements and inference rules · Chapters 1–3
1. Separate truth, proof, checking and search
Construct and measure proofs · Chapters 4–6
4. Count a complete chain refutation
Compare resources and systems · Chapters 7–9
7. Keep proof length and working space separate
Connect evidence and applications · Chapters 10–12
10. Understand the NP and coNP connection without overclaiming
Diagnose and practise · Chapters 13–14
CHAPTER 1 OF 14 · Read statements and inference rules
1. Separate truth, proof, checking and search
Four questions with different answers
Suppose a collection of constraints cannot all hold together. First ask whether that claim is true. Next ask what counts as a proof of it. Then ask how a supplied proof can be checked. Finally ask how to find such a proof without already knowing its useful intermediate steps. These questions interact, but answering one does not automatically answer the others.
A truth table can establish that a formula with four Boolean variables has no satisfying assignment by checking all sixteen assignments. A different certificate might contain only a few inference steps. The first method establishes the answer through exhaustive evaluation; the second provides a derivation whose individual transitions can be inspected. Neither description alone tells us how long a particular program spent discovering the certificate.
Think of a completed maze route and the exploration that found it. A route can avoid every dead end even though its finder visited many of them. The analogy explains the distinction between an output and its discovery history. It does not establish a complexity theorem: formal bounds need an input encoding, a family of instances and a specified computational model.
A precise object to minimise
Fix a proof system P. For a statement A that P proves, let sP(A) be the size of its smallest P-proof, using an agreed measure such as the number of encoded symbols. This is a mathematical minimum over all valid proofs, not the length of the first proof returned by a search program.
If we exhibit a proof of size 80, we establish sP(A) ≤ 80. We have not established equality. A claim that every proof requires at least 80 needs an argument covering every permitted derivation, including ones nobody has yet discovered. This change from “here is one” to “there cannot be a smaller one” is the essential shift from an upper bound to a lower bound.
Start a proof-cost notebook with four entries: the exact input, the legal rules, the measurement convention and the claim being tested. A reader should be able to distinguish a semantic conclusion from an efficiency claim before reading the calculation.
CHAPTER 2 OF 14 · Read statements and inference rules
2. Read Boolean constraints without losing their meaning
Literals, clauses and conjunctions
A Boolean variable takes one of two truth values. A literal is a variable such as p or its negation ¬p. A clause is a disjunction of literals: p ∨ q is true when at least one of p and q is true. A formula in conjunctive normal form, abbreviated CNF, requires every listed clause to be true. The outside connection between clauses is “and”.
Consider the three clauses p ∨ q, ¬p ∨ q, and ¬q. The first two force q to be true: if q were false, one would require p and the other would require ¬p. The third requires q to be false. Therefore no assignment satisfies all three. This explanation identifies a contradiction without confusing a clause with a whole formula.
There are four assignments to p and q. When q is true, ¬q fails regardless of p. When q is false and p is false, p ∨ q fails. When q is false and p is true, ¬p ∨ q fails. Those four cases provide an independent semantic check of the answer.
Two empty objects that mean opposite things
The empty clause contains no literal that could be true, so it is false. We write it as □. A CNF containing that clause is unsatisfiable. By contrast, an empty collection of clauses imposes no restrictions and is satisfied by every assignment. Removing all clauses and deriving an empty clause are entirely different operations.
For a small parser or hand calculation, write clauses as sets of signed variables. Repeated occurrences of p within one clause do not add a new condition. A clause containing both p and ¬p is always true. These conventions make counting easier, but a file format may impose its own restrictions on duplicates and tautological clauses.
Before optimising a proof, translate one clause back into ordinary language. If ¬a ∨ b means “if a, then b”, check both directions carefully: it does not say that b implies a. A mistaken translation can produce a perfectly valid proof about the wrong problem.
CHAPTER 3 OF 14 · Read statements and inference rules
3. Understand why the resolution rule is sound
Cancel one complementary pair
Resolution takes clauses C ∨ p and D ∨ ¬p and infers C ∨ D. The selected variable p is the pivot. Here C and D denote the other literals, which are retained. Duplicates in the resulting clause can be collapsed under the set convention.
Why is this sound? Assume an assignment satisfies both parent clauses. If p is false, the first parent requires C. If p is true, the second requires D. Either way C ∨ D holds. The argument covers both possible values of the pivot, so the conclusion follows from the parents.
For the example in Chapter 2, resolving p ∨ q with ¬p ∨ q produces q. Resolving q with ¬q produces □. The refutation consists of three input clauses and two derived clauses. Each derived line names its parents and pivot; the final empty clause establishes that the inputs cannot all be true.
An attractive but invalid cancellation
From p ∨ q and ¬p ∨ ¬q, resolving on p produces q ∨ ¬q, a tautology. It does not produce □ by simultaneously cancelling both complementary pairs. The assignment p=true, q=false satisfies both parents, so any claimed contradiction from these two clauses alone must be wrong.
This is a useful first-error diagnostic. A line may look shorter and more decisive precisely because it has discarded information illegally. Repair begins by restoring the unselected literals, not by finding a more persuasive verbal explanation for the incorrect line.
Resolution is complete for refuting unsatisfiable propositional CNF formulas: every such formula has a resolution refutation. Completeness concerns existence, not a promise of short proofs. Nordström’s lecture on resolution and the pigeonhole principle develops the calculus and its limitations. Our small calculations use ordinary resolution only; additional transformations used by practical solvers require their own justification.
CHAPTER 4 OF 14 · Construct and measure proofs
4. Count a complete chain refutation
State the instance and every inference
Let x0, x1, x2, x3 and x4 be Boolean variables. The six input clauses are x0; ¬x0 ∨ x1; ¬x1 ∨ x2; ¬x2 ∨ x3; ¬x3 ∨ x4; and ¬x4. In words, the first condition holds, each condition implies the next, and the last condition is forbidden.
Label those inputs C1 through C6 in the order given. Derive C7=x1 from C1 and C2, pivot x0. Derive C8=x2 from C7 and C3, pivot x1. Derive C9=x3 from C8 and C4, pivot x2. Derive C10=x4 from C9 and C5, pivot x3. Finally derive C11=□ from C10 and C6, pivot x4.
There are five resolution inferences. If proof length counts all displayed clauses, including inputs, the length is eleven. If a convention counts only derived lines, it is five. Both counts are legitimate descriptions once their conventions are stated; presenting them as conflicting measurements would be misleading.
Count symbols separately from lines
Under the simple measure “total literal occurrences in displayed clauses”, the inputs contribute 1 + 2 + 2 + 2 + 2 + 1 = 10. The four derived unit clauses contribute four more; the empty clause contributes zero. The total is fourteen literal occurrences. The maximum clause width is two.
This literal count excludes punctuation, variable-name lengths, line numbers and parent references. It is therefore not a byte count for a proof file. An implementation needs an actual encoding before comparing storage requirements or checker throughput.
Generalise the construction to m implications linking x0 through xm, with x0 and ¬xm as endpoint clauses. For m ≥ 1, the displayed proof has m+2 input lines, m+1 derived lines, 2m+3 lines altogether and 3m+2 literal occurrences. Substituting m=4 recovers eleven and fourteen. These are explicit upper bounds supplied by this construction, not a benchmark obtained by running a SAT solver.
CHAPTER 5 OF 14 · Construct and measure proofs
5. Distinguish a construction from a lower-bound argument
Change one clause and look for a witness
The chain is unsatisfiable because every link carries truth towards the forbidden endpoint. Remove ¬x1 ∨ x2. Now x0=true, x1=true, x2=false, x3=false and x4=false satisfies every remaining clause. The missing link allows the truth value to change at that position.
The same reasoning works for any removed implication: set variables before the break to true and variables after it to false. Remove the starting unit instead, and the all-false assignment works. Remove the ending unit, and the all-true assignment works. Thus every input clause is necessary for the unsatisfiability of this particular chain formula.
This proves that the input is minimally unsatisfiable: deleting any one input clause makes it satisfiable. It does not, by itself, calculate the minimum length of a refutation. “No input can be removed” and “no shorter derivation exists” are different optimisation questions.
Measure growth across a family
A lower bound becomes a complexity result when it applies systematically as an instance parameter grows. We might study the smallest proof size for every member Fm of a family, rather than compare two hand-selected examples. The parameter m, number of variables and full encoded input size may differ, so the denominator of a growth claim must be explicit.
The chain family has a linear-size construction. An exponential lower bound cannot hold for these same proofs under the displayed line-count convention, because the construction already provides short witnesses. Trying a slow search procedure on a long chain does not change that mathematical upper bound.
Conversely, observing fast behaviour on chains does not show that all CNF formulas have short proofs. Chains expose a favourable structure: each unit leads directly to the next. Good experimental design deliberately varies structure, not only the number of variables. Record whether an instance is a chain, a counting constraint, a parity condition or a mixture before generalising from runtime.
CHAPTER 6 OF 14 · Construct and measure proofs
6. See how sharing changes the representation of a proof
A lemma can be written once and used again
A derivation can be represented as a tree, with each occurrence of a premise attached to a particular use, or as a directed acyclic graph in which a previously established lemma can support several later inferences. The graph records sharing. Unfolding it into a tree may repeat the entire derivation of a shared lemma.
For an accounting example, suppose a fixed derivation of lemma L contains eight inference nodes. Three later branches each use L once and each adds one inference. Storing L’s derivation once gives eight shared nodes plus three branch nodes: eleven. Unfolding those three uses into separate copies gives 3 × 8 + 3 = 27 nodes in the corresponding portion of the tree.
Any identical final combination of the branches would add the same number of nodes to both totals. The difference of sixteen comes from duplicated work in this representation. This calculation describes one specified derivation and its unfolding. It does not prove that every tree proof of the final statement needs twenty-seven nodes; another derivation might avoid this lemma entirely.
A smaller description is not an unchecked shortcut
Sharing requires valid references. A checker must establish L before accepting a later use of it. A reference to a missing line, a circular dependency or a changed version of the lemma is not proof compression; it is a broken derivation.
Abbreviations raise a related issue. A fresh symbol can stand for a compound expression if the proof system explicitly permits the definition and its use. One cannot silently add arbitrary new assumptions and then compare the shorter result with proofs in a system that forbids them.
The founding Cook–Reckhow paper compares propositional systems and studies extensions that introduce abbreviations. For a learner, the immediate habit is simpler: write down whether reuse, definitions and substitution are allowed before making a size comparison. A proof’s representation is part of the claim, not packaging to be ignored afterwards.
CHAPTER 7 OF 14 · Compare resources and systems
7. Keep proof length and working space separate
Replay the chain with a small working set
The eleven-line chain proof does not require all eleven clauses to remain active simultaneously. Begin with x0. Bring in ¬x0 ∨ x1, derive x1, then erase the two parents. Keep x1, bring in ¬x1 ∨ x2, derive x2, then erase the parents. Continue until x4 and ¬x4 yield □.
In a configuration model that counts a newly derived clause before deleting its parents, this schedule has at most three clauses present at once. At an intermediate inference they are a unit, a binary clause and the new unit. Their total literal count is four. At the last inference the two unit parents and empty clause contain two literals altogether.
The claimed bounds assume input clauses can be downloaded when needed and erased afterwards. If an implementation keeps its entire input resident, its physical memory includes that storage. A theoretical clause-space calculation and a process’s measured memory usage are not interchangeable numbers.
Deletion trades memory against future work
Erasing a lemma is harmless if it will never be needed again. If it is needed later, it must be retained, reloaded under the model’s rules, or rederived. A useful scheduling exercise therefore marks the last use of each clause, rather than deleting the largest-looking clause without considering dependencies.
This makes proof space a question about the sequence of configurations, not just the final proof graph. Two schedules for the same graph can retain different amounts of information. Similarly, a proof with few lines can contain very large clauses, so a clause count alone may understate the information being stored.
Nordström’s study of pebble games and proof-space trade-offs gives the formal framework and explains why length, width and space require separate analysis. Our chain schedule illustrates their distinction but does not establish a general trade-off theorem. Its especially simple dependency structure makes the small working set possible.
CHAPTER 8 OF 14 · Compare resources and systems
8. Use width to count the available clauses
A finite counting calculation
The width of a clause is its number of literals. Under the convention that clauses contain no repeated variables and no complementary pair, a width-k clause over n variables is chosen by selecting k variables and then one of two signs for each. There are C(n,k) × 2^k such clauses.
For four variables, the number of possible clauses of width at most two is 1 + 4×2 + 6×4 = 33. The first term counts the empty clause, the second counts eight units, and the third counts twenty-four binary clauses. For twenty variables the corresponding count is 1 + 40 + 190×4 = 801.
These are counts of possible clauses, not proofs. A width-bounded saturation procedure starts with permitted input clauses, repeatedly derives permitted resolvents and records each new clause only once. If a refutation exists within that width restriction, a finite search can eventually find it. The number of possible additions is bounded by the clause count; the work spent examining candidate parent pairs is additional.
A failed restricted search is not a satisfying assignment
Consider p ∨ q, ¬p ∨ q, p ∨ ¬q and ¬p ∨ ¬q. Resolving the first pair yields q. Resolving the second pair yields ¬q. These resolve to □. All input clauses have width two, and the refutation remains within width two.
A procedure that accepts only width-one input clauses would discard all four inputs. Failure to find a contradiction after that restriction tells us nothing about the satisfiability of the original formula. Even when all inputs fit an allowed width, failure under a narrower-than-needed intermediate-width restriction is not a certificate of satisfiability.
The important quantifier is “there exists a proof within this width”. A single wide proof does not demonstrate that width is necessary: a narrower proof may exist. Width becomes a lower-bound tool only when a theorem excludes all narrower proofs. The resolution resource survey places this counting intuition alongside the deeper size–width results.
CHAPTER 9 OF 14 · Compare resources and systems
9. Compare proof systems through what they can express
A three-object allocation contradiction
Suppose three jobs A, B and C must each occupy at least one of two slots, with at most one job in any slot. Introduce six Boolean variables, one for each job–slot pair. Three clauses require each job to use a slot. For each slot, three pairwise negative clauses prevent two different jobs from occupying it. That gives nine clauses in this basic CNF encoding.
There are 2^6 = 64 assignments to inspect if we use a full truth table. None works. Each of the three jobs requires an occupied pair, while the two slots can accommodate at most two occupied pairs. Allowing a job to occupy both slots cannot help; it consumes more capacity.
Now describe the same requirement with zero–one variables and explicit counting inequalities. Summing the three job inequalities says the sum of all six variables is at least three. Summing the two slot-capacity inequalities says that same sum is at most two. Combining them gives the contradiction 3 ≤ 2.
The arithmetic explanation uses a language that can express counts directly. The CNF version represents capacity through pairwise clauses. Both describe the same feasibility question over Boolean assignments, but a formal comparison must include the cost of translating between representations and the rules available for deriving the counting inequalities.
Keep a lower bound attached to its system
The pigeonhole principle is a central example of a simple counting argument whose usual propositional encodings are hard for resolution as the number of objects grows. Haken’s exponential resolution lower bound is discussed in the resolution lecture. That result is not a statement that every possible mathematical proof of the pigeonhole principle is exponentially long.
A system P polynomially simulates Q when Q-proofs can be represented by P-proofs with polynomial size overhead; a p-simulation additionally supplies a polynomial-time translation. Krajíček’s account of the Cook–Reckhow definitions makes the distinction precise. Such comparisons are more informative than declaring one system “stronger” after seeing a single convenient example.
CHAPTER 10 OF 14 · Connect evidence and applications
10. Understand the NP and coNP connection without overclaiming
Verification uses the supplied certificate
In the Cook–Reckhow framework, a propositional proof system has a polynomial-time verification procedure, is sound, and supplies a proof for every tautology. Polynomial verification time is measured in the combined encoded length of the statement and proposed proof. A huge proof can therefore take huge time to check while still meeting that definition.
A system is polynomially bounded if every tautology has some proof whose size is bounded by one polynomial in the statement size. The same polynomial must work across all inputs for that system. Choosing a different convenient polynomial after seeing each individual example would destroy the meaning of the condition.
The fundamental equivalence is that a polynomially bounded propositional proof system exists exactly when NP=coNP. This is not the same assertion as P=NP. The Cook–Reckhow paper supplies the foundational connection; Krajíček’s exposition states the equivalence explicitly. The existence of such a system remains an open problem, rather than a consequence of practical solver success.
Recognise the claim a piece of evidence supports
Suppose a solver produces a short certificate for one thousand test formulas. The observation concerns those formulas and that solver configuration. It does not quantify over every tautology, every size or every permitted proof system. Likewise, a timeout says the run exceeded a resource limit; it does not show that no short certificate exists.
If someone claims that one restricted proof system needs long proofs, ask which family and which measure the lower bound covers. If someone claims that no proof system can have short proofs for all tautologies, the quantifier ranges over every sound, complete, polynomially checkable system. That is a much stronger assertion.
This distinction is useful outside complexity theory. A test suite, an explicit construction and an impossibility theorem are three different kinds of evidence. Describe each at its actual strength. A successful experiment can guide a conjecture without already proving it, and an unresolved general question does not make a particular checked derivation uncertain.
CHAPTER 11 OF 14 · Connect evidence and applications
11. Connect certificates to dependable software reasoning
Keep the input, proof and checker together
An unsatisfiability result becomes independently inspectable when the exact input formula is accompanied by a certificate and a checker that validates the required steps. The checker should be run on the formula actually generated, not a similar-looking later version. Variable renaming, deleted constraints or changed assumptions can invalidate the connection to the original problem.
The DRAT-trim project documentation describes checking clausal certificates with additions and deletions, including transformations beyond ordinary resolution. A DRAT trace should therefore not be described as a plain resolution proof without examining its permitted steps. The certificate format and checker semantics determine what has been established.
For our three-clause example, a simple resolution checker needs only to confirm that q follows from the two named parents and that □ follows from q and ¬q. It should reject a trace that cites a parent not yet available, selects a nonexistent pivot or omits a required literal from the resolvent. Those deliberately broken examples test different failure modes.
A correct certificate can still concern the wrong model
Imagine a scheduling tool that encodes “each job has a slot” but forgets the condition that a particular job requires a specialist room. A proof about the encoded constraints cannot restore the omitted requirement. Trust therefore has two layers: the logical validity of the certificate and the fidelity of the model to the intended problem.
The existing guide to proving software correct before it runs develops that specification boundary through formal verification. Type Theory provides another route into machine-checked evidence and the assumptions behind it.
Privacy is a different property again. An ordinary efficiently checkable certificate need not hide any witness or intermediate reasoning. For that separate question, the specialist guide to zero knowledge and witness indistinguishability distinguishes two privacy guarantees. Do not infer secrecy from the word “proof”.
CHAPTER 12 OF 14 · Connect evidence and applications
12. Transfer the reasoning when the constraints change
Three alterations to the chain
Return to the six-clause chain in Chapter 4. Before doing any algebra, predict what each alteration changes: truth of the constraints, availability of the old proof, or only the length of an available proof. Then give a certificate or satisfying assignment.
First, remove ¬x1 ∨ x2. The assignment true, true, false, false, false to x0 through x4 satisfies the remaining formula. The old line deriving x2 is no longer justified because its implication parent has disappeared. The failure is local and identifiable; later lines cannot repair it by continuing to cite the missing result.
Second, restore the chain but replace ¬x4 with x4. The all-true assignment satisfies every clause. The implication sequence still derives x4, but x4 no longer conflicts with the final input. A derivation of a true endpoint is not itself a contradiction.
Third, restore the original formula and add ¬x0 ∨ x4 as a shortcut clause. Resolve it with x0 to derive x4, then resolve with ¬x4 to derive □. This displayed proof uses three input clauses and two derived clauses, giving five displayed lines and five literal occurrences. The full input now has seven clauses, but only three are needed by this refutation.
Explain what the changed count means
If a reporting convention prints every input clause whether used or not, the shortcut certificate has seven input lines plus two derived lines, so its reported length is nine rather than five. The logical argument is identical; the accounting convention differs. Record whether you are measuring a proof’s used axioms or an entire input-plus-trace file.
The original chain clauses remain valid constraints after adding the shortcut. Adding a consequence can make an available derivation shorter without changing the satisfying assignments. Here the original formula was already unsatisfiable, so the empty set of satisfying assignments remains empty; the useful lesson concerns access to an intermediate implication.
A good transfer answer names the changed assumption, presents its new witness, and states which old inference survives. Merely repeating “the chain leads to a contradiction” misses the precise point at which each modified task diverges.
CHAPTER 13 OF 14 · Diagnose and practise
13. Diagnose common errors and answer useful questions
My proof checks, so have I found the shortest proof?
No. Successful checking establishes validity under the checker’s rules. Minimality needs an additional argument excluding smaller proofs under the same measure. Keep the certificate and the minimality claim in separate parts of your notes. If you only have an explicit construction, report an upper bound.
Does a large truth table prove that every proof is large?
No. A truth table enumerates assignments, whereas a derivation can exploit structure. The implication chain has many possible assignments as it grows but a short refutation. Counting the rows of one method does not lower-bound every other method.
Is clause width the same as memory?
No. Width counts the literals in one clause; clause space counts simultaneously retained clauses under a specified schedule. Total literal space also accounts for their widths. A single broad clause and many narrow clauses stress these measures differently. Translate the theoretical measure into an implementation model before comparing it with bytes.
Can I conclude satisfiable when unit propagation stops?
No. The four binary clauses in Chapter 8 have no initial unit clause, so unit propagation alone makes no initial progress, yet the formula is unsatisfiable. A satisfying assignment must make every original clause true. Failure of one inference procedure to finish is not such an assignment.
What should I repair first in a rejected proof?
Locate the earliest invalid line. Check parent availability, the selected complementary pivot and the exact remaining literals. For an encoding problem, check the translation before the proof trace. For an accounting problem, state whether inputs, repeated uses, literal names and deletion operations count. These are distinct repairs, not interchangeable reasons to restart the whole task.
Does a resolution lower bound limit every solver?
Only an appropriately established connection allows a proof lower bound to imply a limitation on a particular algorithm. A solver may use preprocessing, definitions or reasoning that goes beyond the system being analysed. Conversely, a theorem about an algorithm’s model does not predict every practical runtime. Identify both the formal restriction and the actual implementation behaviour before drawing that conclusion.
CHAPTER 14 OF 14 · Diagnose and practise
14. Build a learning route that produces checkable evidence
A first session: meaning before optimisation
Begin with two variables and list all four assignments for the three-clause contradiction. Write a two-inference resolution trace, naming parents and pivots. Next deliberately attempt the invalid double cancellation from Chapter 3 and find the satisfying assignment that refutes it. This session is complete when you can explain why the valid rule preserves consequences and why the tempting alternative does not.
A second session: measure one construction honestly
Rebuild the implication chain for m=3 and m=5. The formulas in Chapter 4 predict nine and thirteen displayed lines, and eleven and seventeen literal occurrences respectively. Check those numbers directly. Replay each derivation with a three-clause working set and distinguish the stored clauses from the clauses already written to an output trace.
Now add a shortcut or remove an implication. Produce the changed proof or satisfying assignment before recounting anything. If the semantic answer changes, an unchanged performance spreadsheet is not a useful comparison. Save the actual formulas alongside the measurements so another learner can reproduce the result.
A third session: move from examples to research questions
Study the allocation example in both CNF and counting-inequality form. Ask which translations preserve satisfiability, how many variables and clauses they introduce, and what inference rules they make convenient. Then read a theorem with its full quantifiers: proof system, input family, encoding, size parameter and resource bound.
For foundations, use Cook and Reckhow, The Relative Efficiency of Propositional Proof Systems, together with Krajíček, The Cook–Reckhow Definition. For a research route through resolution, algebraic systems and counting, use Proof Complexity as a Computational Lens. For proof memory, follow Pebble Games, Proof Complexity, and Time-Space Trade-offs. For certificate engineering, read the DRAT format and checker documentation.
Carry one precise question into the next problem: what evidence would establish this particular claim? A complete answer might be a satisfying assignment, a checked refutation, a proof construction for a whole family, or a lower-bound theorem. Knowing which object is needed is the first step towards producing reasoning that another person can inspect and use.