Maximal Proof-Search Algorithms on Natural Tautology Sets

Definitions and mathematical statement

Let $\mathrm{TAUT}$ denote the collection of propositional formulas that evaluate to true under every Boolean assignment. The record concerns proof-search pairs $X=(A,P)$, where $A$ searches for proofs in a proof system $P$. It does not specify the admissible proof systems, algorithms, encodings, or termination requirements. Write $\mathcal C$ for the intended class of admissible proof-search pairs; this class remains to be specified from the cited sources.

Write $\mathcal T_{\mathrm{nat}}$ for the intended collection of natural tautology test objects. The original statement refers to "some natural test sets of tautologies," whereas the cleaned statement refers to "a natural family of tautology test sets." Neither naturalness nor the structure and quantification of these test objects is defined in the supplied record. In particular, the record does not determine whether a test object is a single subset of $\mathrm{TAUT}$, a sequence of such subsets, or a family subject to additional conditions.

For a fixed intended test object $S$, write $X\succeq_S Y$ for the supplied but undefined test-set quasi-order comparing running times up to polynomial factors, with the convention that this notation ranks $X$ at least as highly as $Y$. A quasi-order is a reflexive, transitive relation. Relative to such a relation, $X$ is maximal precisely when \[ \forall Y\in\mathcal C,\qquad Y\succeq_S X\ \Longrightarrow\ X\succeq_S Y. \] Thus maximality means that no admissible pair lies strictly above $X$; it does not by definition require $X\succeq_S Y$ for every $Y$.

The existential reading of the original question has the following conditional statement schema: \[ \exists S\in\mathcal T_{\mathrm{nat}}\ \exists X=(A,P)\in\mathcal C\ \forall Y\in\mathcal C,\qquad Y\succeq_S X\ \Longrightarrow\ X\succeq_S Y. \] The problem asks whether such a natural test object and maximal proof-search pair exist. This schema records the intended maximality quantifiers, but is not a complete formalization: the admissible class, test objects, naturalness condition, and running-time quasi-order must be supplied before it determines a mathematical assertion. The cleaned formulation may instead intend a family-level comparison or different quantification over test sets; the supplied evidence does not resolve this.

Short English statement

The question asks whether some natural collection of tautologies supports a proof-search algorithm that cannot be strictly improved under the intended comparison of running times up to polynomial factors. The record leaves the test objects, admissible algorithms and proof systems, and comparison relation undefined, so the displayed statement is a conditional schema requiring mathematical review.

Sources

• Local registry: data/unsolvedmath/problems.json, permanent UnsolvedMath ID $30004556$, source problem code catalogue entry, title "Maximal Proof-Search Algorithms on Natural Tautology Sets." The supplied record gives proposed year 2020 and names no proposer.
• Supplied source citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2021), Oberwolfach Reports, pp. 1693--1757, DOI https://doi.org/10.4171/owr/2020/34. The background describes these reports as records of mathematical workshops and their open-problem discussions.
• Supplied literature source: Krajicek, "Proof Search Problem," https://eccc.weizmann.ac.il/report/2021/053/.
• Supplied literature source: "Oberwolfach Report 34/2020," https://doi.org/10.4171/owr/2020/34.
• Literature assessment dated exactly 2026-08-22: the supplied curation labels the problem open and states that no unconditional construction is known of a natural test set supporting a $\succeq$-maximal proof-search algorithm, and that the problem remains explicitly open in the current proof-complexity literature. This is supplied dated curation derived from the OWR record, not an independently verified literature assessment; its time-sensitive status and cited claims require independent verification.
• The registry labels the statement corrected_verified and says that mathematical content was preserved while notation, typography, omitted definitions, or duplicate clauses were repaired for self-contained publication. These are supplied editorial assertions, not independent verification of this draft or of the missing definitions.