The problem
The same logical truth can have different explanations. “A switch is on or it is not” can be checked by listing its two possible settings, or justified by a rule that directly recognizes this form. Both arguments can be checked, but longer formulas can have very different proof lengths in different methods. Is there one efficiently checkable proof method whose proofs can match every other such method with an overhead bounded by a fixed power of the other proof’s length?[1] [2]
Different formal proof systems can require different amounts of written evidence for the same propositional tautology, a formula true under every Boolean assignment. The open question is whether one efficiently checkable system matches every other system’s proof lengths within a polynomial overhead. A Cook–Reckhow system is represented by a polynomial-time computable function whose range is exactly , the set of tautologies: a proof string is mapped to the formula it proves. System simulates system when, for some polynomial , every -proof has an -proof of the same formula with . The polynomial may depend on , but not on the particular proof. An optimal simulates every ; ordinary simulation does not require an efficient procedure for finding .[1] [2]
Scope
Does TAUT admit a Cook–Reckhow proof system f that simulates every such system g: for each g some polynomial p bounds an f-proof of g(π) by p(|π|) for every g-proof π? Translation need not be computable efficiently.
What remains open
The cited 2026 oracle constructions establish barriers for approaches that remain valid after supplying a common external answer source to computations. They do not decide whether ordinary tautologies have an optimal proof system. The stronger requirement of efficiently translating proofs gives p-optimality; solving that variant is not the definition of ordinary optimality used here.[1] [2]
Why it matters
Proof length is a cost even after the truth of a statement is known: it determines how much evidence must be written down and checked. Comparing proof methods asks whether a long explanation reflects an unavoidable burden or just the method chosen to express it. A universal benchmark would provide a common basis for this comparison across all efficiently checkable methods.[1] [2]
A common comparison standard would help distinguish limitations of a particular proof representation from the relative strength of other efficiently checkable methods. Optimality would not by itself give every tautology a proof bounded by one fixed polynomial in its formula length. It bounds proof length in the chosen system relative to proofs in each other fixed system; a polynomial bound in formula length is a separate requirement. This distinction links two questions in proof complexity: how systems compare, and whether every tautology has a short certificate.[1] [2]
Definitions
4 terms
tautology
A propositional formula true under every Boolean assignment; TAUT denotes the set of these formulas.[2]
proof system
Here, a sound and complete formal method for proving propositional tautologies with efficiently checkable proofs. A Cook–Reckhow function maps proof strings to exactly the tautologies.[1]
simulation
A comparison in which every proof in one system has a proof of the same conclusion in another system with polynomial length overhead. The polynomial may depend on the first system.[1]
p-optimality
A stronger version of optimality that requires polynomial-time translation from every other proof system, instead of only the existence of short replacement proofs.[1]
Sources
- The SPARSE-Relativization Framework and Applications to Optimal Proof Systems
Notes on The SPARSE-Relativization Framework and Applications to Optimal Proof Systems
Exact February 2, 2026 version: selected abstract and §2 define length simulation versus efficient p-simulation, with the main constructions in oracle models. These do not decide ordinary optimality for TAUT.
- Recursive Jump Operators and Optimal Proof Systems
Notes on Recursive Jump Operators and Optimal Proof Systems
July 1, 2026 conference article: selected introduction defines optimal proof systems by polynomial proof-length simulation, states the TAUT question as open and separates existential from constructive non-optimality. Full proofs were not audited.