Provability of P vs. NP in algorithmically verifiable mathematics (AV-mathematics)

Hromkovič and Rossmanith (JCSS 2020) study what can be proved inside “AV-mathematics”: any fixed consistent and sufficiently powerful formal theory whose proofs can be verified algorithmically (PA, ZFC, and stronger theories included). They prove that for every such system there are infinitely many concrete algorithms whose polynomial-time status, and whose failure to solve SATISFIABILITY, is unprovable, and they construct a concrete SAT-solving algorithm $X_1$ for which neither “works in polynomial time” nor “solves SATISFIABILITY” is provable. However, a proof of $\mathrm{P}\neq\mathrm{NP}$ would make the disjunction “X does not work in polynomial time or X does not solve SATISFIABILITY” provable for every algorithm $X$, and the authors show this disjunction is provable for all their constructions — so their results leave the provability of $\mathrm{P}\neq\mathrm{NP}$ itself untouched. The problem they leave open is to determine the provability status of $\mathrm{P}\neq\mathrm{NP}$ in a given AV-formal system. Since a proof of $\mathrm{P}\neq\mathrm{NP}$ in the system would make the disjunction “$X$ does not work in polynomial time or $X$ does not solve SATISFIABILITY” provable for every algorithm $X$, exhibiting a concrete algorithm for which this disjunction is unprovable would establish that $\mathrm{P}\neq\mathrm{NP}$ is unprovable in that system.

Background

The question whether $\mathrm{P}$ equals $\mathrm{NP}$ asks whether every computational problem whose solutions can be checked efficiently can also be solved efficiently. Here $\mathrm{P}$ is the class of languages decidable by deterministic Turing machines in polynomial time, $\mathrm{NP}$ the class decidable in nondeterministic polynomial time, and SATISFIABILITY (SAT) — deciding whether a Boolean formula in conjunctive normal form has a satisfying assignment — is the canonical NP-complete problem, so $\mathrm{P}=\mathrm{NP}$ holds exactly if SAT admits a polynomial-time algorithm. The question has been open since the early 1970s.

Several classical results suggest that $\mathrm{P}$ vs. $\mathrm{NP}$ may resist ordinary proof techniques. Baker, Gill and Solovay (1975) constructed oracle worlds in which $\mathrm{P}=\mathrm{NP}$ and others in which $\mathrm{P}\neq\mathrm{NP}$, so any proof settling the question must use non-relativizing arguments. Razborov and Rudich (1997) showed that a wide class of “natural” combinatorial proof techniques (natural proofs) cannot prove superpolynomial circuit lower bounds unless strong pseudorandom generators do not exist. Aaronson (2003) surveyed the further possibility that $\mathrm{P}$ vs. $\mathrm{NP}$ might be formally independent — unprovable — in standard axiom systems such as ZFC (Zermelo–Fraenkel set theory with the axiom of choice, the usual foundation of mathematics).

Hromkovič and Rossmanith (2020) gave this metamathematical discussion a precise, fully formal framework. They call algorithmically verifiable mathematics (AV-mathematics) any fixed formal theory that is consistent, sufficiently powerful to speak about algorithms and computational complexity, and for which an algorithm decides, given a text, whether it is a valid proof; every ordinary system such as Peano arithmetic (PA) or ZFC is an AV-mathematics. Gödel's incompleteness theorem (1931) already shows that such systems cannot prove all true arithmetic statements, and Chaitin's information-theoretic refinement (1974) sharpens this for Kolmogorov complexity $K(x)$ — the length of the shortest program producing the string $x$ — by showing that in a fixed formal system only finitely many lower bounds of the form “$K(x)\ge n$” are provable. The paper calls a decision problem $L$ almost everywhere solvable if for all but finitely many inputs $x$ one can prove either “$x\in L$” or “$x\notin L$” in AV-mathematics.

Within this framework the paper proves, relative to an arbitrary fixed AV-formal system: a provability analogue of Rice's theorem (Rice's classical theorem of 1953 states that every nontrivial semantic property of programs is undecidable; the provability version states that for every nontrivial semantic property of machines there are infinitely many concrete machines whose membership in the property is unprovable); infinitely many algorithms for which neither polynomial-time nor non-polynomial-time status is provable; infinitely many algorithms for which it is unprovable that they do not solve SAT; and — via an explicit construction $X_{A,B,f}(M)$ whose accepted language and running time depend on whether an embedded machine $M$ halts on the empty input — a concrete algorithm $X_1$ that is provably an algorithm and in fact solves SATISFIABILITY (a fact not provable in the system), while the system proves neither “$X_1$ works in polynomial time” nor “$X_1$ solves SATISFIABILITY”.

The critical subtlety is the logical form of a separation. If $\mathrm{P}\neq\mathrm{NP}$ is provable in an AV-formal system, then for every algorithm $X$ the disjunction

$\text{“}X\text{ does not work in polynomial time or }X\text{ does not solve SATISFIABILITY”}\quad(*)$

is provable, by instantiating the theorem with $X$. The paper's constructions are provably useless for reversing this implication: for every machine of the constructed form $X_C(M)$, the disjunction $(*)$ is provable even though neither disjunct is — an “uncertainty principle” for algorithmic properties. Thus the paper's unprovability phenomena for individual properties do not touch the provability of $\mathrm{P}\neq\mathrm{NP}$ itself.

On the constructive side, the paper proves that certain class equalities carry automatic (almost) constructive content: if $\mathrm{P}=\mathrm{NP}$ is provable in AV-mathematics then a single explicit algorithm $S$ provably decides SAT in polynomial time, correctly rejecting every unsatisfiable formula and correctly accepting all but finitely many satisfiable ones; a concrete deterministic logarithmic-space algorithm for graph reachability (given directed graph, decide whether a path leads from a source to a target vertex) exists if and only if $\mathrm{LOGSPACE}=\mathrm{NLOGSPACE}$ (deterministic vs. nondeterministic logarithmic space); if graph isomorphism — deciding whether two graphs are identical up to a renaming of vertices — lies in $\mathrm{P}$, then a fixed randomized algorithm decides it in expected polynomial time, correctly on all no-instances and on all but finitely many yes-instances, with error probability at most $2^{-n^2}$ on the rest; and $\mathrm{BPP}=\mathrm{PSPACE}$ (bounded-error randomized polynomial time vs. polynomial space) holds if and only if a concrete randomized algorithm solves QBF — deciding the truth of quantified Boolean formulas, the PSPACE-complete problem — in expected polynomial time. Finally, if $\mathrm{P}=\mathrm{NP}$ is not provable, then already the classes of languages that carry machine-verified polynomial-time membership proofs differ, so the “provably certified” version of $\mathrm{P}$ vs. $\mathrm{NP}$ is strictly separated.

These results sharpen, but do not answer, the meta-question standing behind them: can $\mathrm{P}\neq\mathrm{NP}$ be proved at all inside any fixed AV-formal system — or can one exhibit a concrete algorithm for which even the disjunction $(*)$ is unprovable, thereby establishing that $\mathrm{P}\neq\mathrm{NP}$ is unprovable in that system?

Problem Statement

Determine what algorithmically verifiable mathematics — any fixed consistent and sufficiently powerful formal theory whose proofs can be checked by an algorithm — can prove about $\mathrm{P}$ vs. $\mathrm{NP}$. The problem, as explicitly left open by Hromkovič and Rossmanith (2020), is the provability of the separation:

Is $\mathrm{P}\neq\mathrm{NP}$ provable in a given AV-formal system (for instance ZFC)? Here the system is a fixed standard theory of the kind the source treats (for instance ZFC or PA), not a theory obtained by adjoining $\mathrm{P}\neq\mathrm{NP}$ or its negation as an axiom. The source proves the one-directional implication: a proof of $\mathrm{P}\neq\mathrm{NP}$ in the system would make the disjunction $(*)$ — “$X$ does not work in polynomial time or $X$ does not solve SATISFIABILITY” — provable for every algorithm $X$. Consequently, by contraposition, exhibiting a concrete algorithm $X$ for which $(*)$ is unprovable would establish that $\mathrm{P}\neq\mathrm{NP}$ is unprovable in that system. The source proves no converse equivalence: the nonexistence of such a witness yields at most the truth of $\mathrm{P}\neq\mathrm{NP}$ (the source's Theorem 8 derives witnesses with unprovable $(*)$ from the truth of $\mathrm{P}=\mathrm{NP}$), not its provability in the fixed system. The source also proves that its halting-controlled constructions, including $X_1$, cannot be such witnesses ($(*)$ is provable for all of them, though neither disjunct is), so a resolution requires genuinely new machinery. A positive answer — a proof of $\mathrm{P}\neq\mathrm{NP}$ inside such a fixed standard theory — is exactly a resolution of the $\mathrm{P}$ vs. $\mathrm{NP}$ problem itself.

References

1. Juraj Hromkovič, Peter Rossmanith: What one has to know when attacking P vs. NP. Journal of Computer and System Sciences 107 (2020) 142–155. DOI: 10.1016/j.jcss.2019.06.004, https://doi.org/10.1016/j.jcss.2019.06.004 (source paper)
2. Juraj Hromkovič, Peter Rossmanith: What One Has to Know When Attacking P vs. NP (Extended Abstract). In: Proceedings of the 22nd International Symposium on Fundamentals of Computation Theory (FCT 2017), pp. 11–28. DOI: 10.1007/978-3-662-55751-8_2, https://doi.org/10.1007/978-3-662-55751-8_2
3. Juraj Hromkovič: Why the Concept of Computational Complexity is Hard for Verifiable Mathematics. ECCC Technical Report TR15-159 (2015). https://eccc.weizmann.ac.il/report/2015/159/ (identifier: ECCC TR15-159)
4. Juraj Hromkovič: Kolmogorov complexity and nondeterminism versus determinism for polynomial time computations. ECCC Technical Report TR21-049 (2021). https://eccc.weizmann.ac.il/report/2021/049/ (identifier: ECCC TR21-049)
5. Juraj Hromkovič: Kolmogorov complexity and nondeterminism versus determinism for polynomial time computations. Theoretical Computer Science 1013 (2024), article 114747. DOI: 10.1016/j.tcs.2024.114747, https://doi.org/10.1016/j.tcs.2024.114747
6. Scott Aaronson: Is P Versus NP Formally Independent? Bulletin of the European Association for Theoretical Computer Science 81 (2003) 109–136. No DOI; DBLP record: https://dblp.org/rec/journals/eatcs/Aaronson03; author's open-access copy: https://scottaaronson.com/papers/pnp.pdf
7. Theodore P. Baker, John Gill, Robert Solovay: Relativizations of the P =? NP Question. SIAM Journal on Computing 4(4) (1975) 431–442. DOI: 10.1137/0204037, https://doi.org/10.1137/0204037
8. Alexander A. Razborov, Steven Rudich: Natural Proofs. Journal of Computer and System Sciences 55(1) (1997) 24–35. DOI: 10.1006/jcss.1997.1494, https://doi.org/10.1006/jcss.1997.1494
9. Gregory J. Chaitin: Information-Theoretic Limitations of Formal Systems. Journal of the ACM 21(3) (1974) 403–424. DOI: 10.1145/321832.321839, https://doi.org/10.1145/321832.321839
10. H. Gordon Rice: Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74 (1953) 358–366. DOI: 10.1090/S0002-9947-1953-0053041-6, https://doi.org/10.1090/S0002-9947-1953-0053041-6
11. Kurt Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38 (1931) 173–198. DOI: 10.1007/BF01700692, https://doi.org/10.1007/BF01700692
12. William I. Gasarch: Guest Column: The Second P=?NP Poll. ACM SIGACT News 43(2) (2012) 53–77. DOI: 10.1145/2261417.2261434, https://doi.org/10.1145/2261417.2261434
13. Igor C. Oliveira: Meta-Mathematics of Computational Complexity Theory. arXiv:2504.04416 (2025). https://arxiv.org/abs/2504.04416
14. Arne Hole: Constructive solvability and the P versus NP problem. arXiv:2406.16843 (2024). https://arxiv.org/abs/2406.16843