Consider the claim that n+1 pigeons cannot be placed into n holes without two of them sharing a hole. Any competent mathematician sees why it holds in a single sentence. Encode it propositionally and give it to a resolution prover, and the result is very different: for n around twenty, the machine runs without stopping. In 1985 Armin Haken proved that this is not an implementation defect. Every resolution refutation of the pigeonhole formulas has size exponential in n.

This gap, between how easy a truth looks and how hard it is to derive mechanically, sits at the centre of automated theorem proving. It is also one case of a deeper asymmetry. Checking a proof is cheap: a kernel walks the derivation line by line and confirms each inference. Finding the proof is a different problem. The difference between the two comes from complexity class, so more engineering effort cannot remove it.

Kurt Gödel saw the outline of this problem in a 1956 letter to John von Neumann. He asked how quickly a machine could decide whether a statement has a proof of length n. In modern terms, that question is a version of P versus NP. This article covers why proof search resists efficient mechanisation and what completeness actually costs. It also covers how working provers such as Vampire, E, Z3, and Lean-based systems manage when the worst case is often catastrophic.

Begin with verification. Given a candidate proof in a standard system, such as natural deduction, sequent calculus, or a resolution refutation, checking it means confirming that each step applies a valid rule to earlier lines. For propositional systems this takes time polynomial in the length of the proof. For first-order systems with explicit substitutions it remains efficient. This is why the de Bruijn criterion works: Coq, Lean, and Isabelle send every proof through a small trusted kernel, and that kernel can be audited independently of the elaborate machinery that produced the proof.

Search reverses the situation. Propositional tautology is coNP-complete, so a polynomial-time method for finding propositional proofs would collapse coNP into P. Cook and Reckhow sharpened this in 1979. They showed that a proof system in which every tautology has a polynomial-size proof exists if and only if NP equals coNP. Much of the field of proof complexity consists of proving superpolynomial lower bounds for progressively stronger proof systems, one system at a time.

First-order logic is worse. Church and Turing showed in 1936 that first-order validity is undecidable. Gödel's completeness theorem guarantees that every valid formula has a proof, which makes validity recursively enumerable: list candidate proofs, check each one, and halt on success. But this procedure only semi-decides validity. On an invalid input it runs forever, and no finite amount of waiting can tell 'not yet found' apart from 'does not exist'.

So the asymmetry has layers. Verification is polynomial. Bounded search asks whether a proof of length at most n exists, and for reasonable systems it is NP-complete. This is exactly Gödel's question to von Neumann. Unbounded search is undecidable. Each layer reflects the same fact: a proof is a short certificate, and a certificate is easy to check because the hard work of choosing it has already been done elsewhere.

This has a practical consequence that is often overlooked. In modern verification systems, the real division of labour is not between humans and machines. It is between untrusted search and trusted checking. Tactics, hammers, and neural generators can be as heuristic as they like, even unsound, because nothing they produce is accepted until the kernel checks it. The asymmetry that makes discovery hard also makes aggressive, unprincipled search safe.

Takeaway

A proof is a certificate whose difficulty has been paid in advance. Systems that separate untrusted search from trusted checking turn that asymmetry from an obstacle into a design principle.

Completeness is a guarantee about the limit: if a proof exists, the procedure eventually finds it. It says nothing about when. Robinson's 1965 resolution principle, combined with unification, gave first-order logic a refutation-complete calculus with a single inference rule. That elegance hid the cost. Resolution generates clauses combinatorially, and a fair search must eventually consider every derivable clause. In practice the clause set keeps growing until memory runs out, so resource limits end the run before the logic does.

Lower bounds make the cost concrete. Haken proved exponential lower bounds on resolution size for pigeonhole formulas. Urquhart extended them to Tseitin formulas on expander graphs. Ben-Sasson and Wigderson connected resolution size to clause width, which gave a general method for proving such bounds. CDCL solver runs correspond to resolution refutations, so every resolution lower bound is also a lower bound on CDCL runtime. Pipatsrisawat and Darwiche showed that CDCL with restarts can also polynomially simulate resolution, so the correspondence holds in both directions. No branching heuristic can get around it.

Stronger proof systems shorten proofs but make search harder. Extended Frege proves the pigeonhole principle in polynomial size. Nobody knows how to search Extended Frege efficiently, because its power comes from introducing new definitions, which is an unbounded and unstructured choice. Cut-free sequent calculi have the subformula property, which constrains search. However, Statman and Orevkov showed that eliminating cuts can enlarge proofs non-elementarily. A short proof that uses cuts may have no cut-free proof shorter than a tower of exponentials.

Gödel's speed-up theorem goes further. Moving from a theory to a stronger one can shorten some proofs by more than any computable function. One example is moving from n-th order arithmetic to order n+1. Proof length is therefore not an intrinsic property of a theorem. It is a property of a theorem relative to a system, and the systems best suited to search are often those in which proofs are longest.

Herbrand's theorem shows the same tension at the foundations. A first-order formula is unsatisfiable exactly when some finite set of its ground instances is propositionally unsatisfiable. A complete procedure must therefore be ready to enumerate instances without bound, and the number of instances needed can be enormous. Completeness is bought by a willingness to explore everything, and bounded resources make exploring everything impossible.

Takeaway

Completeness guarantees arrival, not a schedule. The calculi easiest to search tend to have the longest proofs, and the calculi with short proofs tend to be the ones nobody can search.

Modern first-order provers such as Vampire and E are built around the given-clause algorithm, inherited from Otter. Clauses are split into processed and unprocessed sets. At each step the prover selects one unprocessed clause and performs all inferences between it and the processed clauses. The results are simplified and then queued. Completeness depends on fairness, meaning every clause must eventually be selected. Provers maintain fairness with an age-weight ratio that alternates between picking the oldest clauses and the lightest ones.

The calculus itself is restricted to shrink the search space. Superposition, developed by Bachmair and Ganzinger, handles equality using term orderings that rule out most rewrites. Literal selection further limits which literals can take part in inferences. These restrictions discard redundant derivations while preserving completeness. Simplification matters just as much: subsumption, demodulation, and redundancy elimination remove clauses that cannot contribute. In practice, provers spend more effort deleting clauses than generating them.

Where theory runs out, portfolios take over. In the CASC competition, Vampire runs dozens of strategies in separate time slices. Many of them are individually incomplete, such as aggressive selection functions or limited-resource strategies that discard clauses unlikely to be processed in time. The ensemble gives up the completeness of any single strategy in exchange for coverage across many kinds of problems. SMT solvers such as Z3 and cvc5 take a different route through DPLL(T). They pass propositional structure to CDCL and delegate theory reasoning to specialised decision procedures.

Premise selection deals with the fact that real problems arrive with thousands of irrelevant axioms. SInE ranks axioms by how rare their symbols are. Isabelle's Sledgehammer uses MePo and the learned MaSh filter to pass a few hundred lemmas to external provers. ENIGMA trains classifiers to guide clause selection in E. Each of these heuristics gives up worst-case guarantees for better empirical results. Each is judged by benchmark performance rather than by a theorem.

The newest strategy uses the asymmetry directly. Systems such as AlphaProof and DeepSeek-Prover use large models to generate candidate Lean proofs and submit them to the kernel, often sampling thousands of attempts. The generator is incomplete, unsound, and opaque. None of that matters, because verification is cheap and trustworthy. Learning cannot overcome the lower bounds, which concern worst cases. It bets instead that the theorems mathematicians care about are not worst cases.

Takeaway

Practical provers do not refute the hardness results; they bet against the worst case. Every heuristic is a hypothesis about which theorems people actually want proved.

The hardness of proof search is not a temporary obstacle that better hardware will remove. It follows from coNP-completeness, from undecidability, and from explicit lower bounds on specific proof systems. Any claim of an efficient general-purpose prover is implicitly a claim about NP versus coNP.

For theoretical logic, this means proof systems should be studied as objects with complexity profiles. The question is not only whether a calculus is complete. It is also how long its proofs are and how searchable its space is. Those two properties pull in opposite directions, and characterising the trade-off remains an open problem.

For practical AI, the lesson concerns system design. Reasoning systems should be built around the gap between finding and checking. Search can then be as heuristic and learned as necessary, while trust rests on small, auditable verifiers. Turing asked whether machines could think. Proof search raises a sharper question: whether they can choose well among exponentially many possibilities, and know when they have.