pith. sign in

arxiv: 2506.16956 · v2 · pith:2Y2O7GZVnew · submitted 2025-06-20 · 💻 cs.CC · cs.LO· math.LO

The Proof Analysis Problem

Noel Arteche , Albert Atserias , Susanna F. de Rezende , Erfan Khaniki This is my paper

Pith reviewed 2026-05-22 00:41 UTC · model grok-4.3

classification 💻 cs.CC cs.LOmath.LO
keywords ResolutionProof Analysis Problemsatisfiability extractionbounded arithmeticExtended Fregelower bounds
0
0 comments X

The pith

Short Resolution proofs of Ref(φ) extract satisfying assignments for φ in polynomial time

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that any short Resolution refutation of the formula Ref(φ), which claims that φ has a small Resolution refutation, can be turned into a satisfying assignment for φ in polynomial time. This affirmatively answers whether short refutations leak the assignment, building on the Atserias-Müller lower bound with a new feasibly constructive proof formalizable in PV1. The authors introduce the Proof Analysis Problem for a proof system Q, which asks if φ is satisfiable given a Q-proof of a Resolution lower bound for φ. They prove this problem is in P for Resolution but NP-complete for Extended Frege.

Core claim

Given any short Resolution refutation of Ref(φ), there is a polynomial-time procedure to extract a satisfying assignment for φ. This follows from a new proof of the Atserias-Müller theorem that is formalizable in Cook's theory PV1 of bounded arithmetic.

What carries the argument

The feasibly constructive proof of the Atserias-Müller lower bound for the Resolution complexity of Ref(φ), which enables direct extraction of satisfying assignments from short refutations.

If this is right

  • Every proof system simulating Extended Frege is weakly automatable if and only if it is weakly automatable when restricted to formulas stating Resolution lower bounds.
  • Ref formulas exist that are exponentially hard for bounded-depth Frege systems.
  • For every strong enough arithmetic theory T, there are unsatisfiable CNF formulas that are exponentially hard for Resolution but on which T cannot prove even quadratic lower bounds.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This extraction technique may generalize to other weak proof systems where lower bounds can be made constructive.
  • The NP-completeness result for Extended Frege suggests that analyzing strong proofs for lower bounds is computationally hard, equivalent to solving SAT.
  • These results highlight a connection between the existence of short proofs of lower bounds and the satisfiability of the original formulas.

Load-bearing premise

That the new feasibly constructive proof of the Atserias-Müller lower bound is correct and can be formalized in PV1, allowing the extraction algorithm to run in polynomial time.

What would settle it

A specific unsatisfiable CNF formula φ together with a short Resolution refutation of Ref(φ) for which no satisfying assignment can be extracted in polynomial time.

read the original abstract

Atserias and M\"uller (JACM, 2020) proved that for every unsatisfiable CNF formula $\varphi$, the formula $\operatorname{Ref}(\varphi)$, stating "$\varphi$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $\varphi$ is satisfiable, Pudl\'ak (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{Ref}(\varphi)$ given a satisfying assignment of $\varphi$. A question that remained open is: do all short Resolution refutations of $\operatorname{Ref}(\varphi)$ explicitly leak a satisfying assignment of $\varphi$? We answer this question affirmatively by giving a polynomial-time algorithm that extracts a satisfying assignment for $\varphi$ given any short Resolution refutation of $\operatorname{Ref}(\varphi)$. The algorithm follows from a new feasibly constructive proof of the Atserias-M\"uller lower bound, formalizable in Cook's theory $\mathsf{PV_1}$ of bounded arithmetic. Motivated by this, we introduce a computational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a proof system $Q$, the Proof Analysis Problem for $Q$ asks, given a CNF formula $\varphi$ and a $Q$-proof of a Resolution lower bound for $\varphi$, encoded as $\neg \operatorname{Ref}(\varphi)$, whether $\varphi$ is satisfiable. In contrast to PAP for Resolution, we prove that PAP for Extended Frege (EF) is NP-complete. Our results yield new insights into proof complexity: (i) every proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas stating Resolution lower bounds; (ii) we provide Ref formulas exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic $T$ we construct unsatisfiable CNF formulas exponentially hard for Resolution but for which $T$ cannot prove even a quadratic lower bound.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that there is a polynomial-time algorithm to extract a satisfying assignment for an unsatisfiable CNF formula φ from any short Resolution refutation of the formula Ref(φ), which encodes that φ has small Resolution refutations. This algorithm is obtained from a new feasibly constructive proof of the Atserias-Müller lower bound, which is formalizable in Cook's theory PV1. The paper introduces the Proof Analysis Problem (PAP) for a proof system Q and proves that PAP for Extended Frege is NP-complete. It also derives several corollaries, including equivalences for automability, exponential hardness for bounded-depth Frege, and limitations for arithmetic theories in proving Resolution lower bounds.

Significance. Assuming the results are correct, this contributes significantly to proof complexity by linking lower bound proofs to explicit computational extraction procedures. The PV1 formalization is a strength because it guarantees that the extraction is feasible and polynomial-time. The NP-completeness result for EF and the insights on automability and hardness provide new tools for analyzing proof systems. This could influence future work on the computational aspects of proof complexity.

major comments (2)
  1. [PV1 formalization and extraction algorithm] The central extraction algorithm depends on the PV1 formalization supplying explicit poly-time witnessing functions for the non-existence of small refutations. The manuscript must clarify (in the section detailing the PV1 proof) that these witnesses are uniformly computable from an arbitrary Resolution derivation of ¬Ref(φ) in time polynomial in the refutation length, without size-dependent advice or oracles; otherwise the claimed polynomial-time procedure does not follow.
  2. [NP-completeness proof for PAP_EF] For the NP-completeness of PAP for EF, the reduction must ensure that both the constructed φ and the EF-proof of the Resolution lower bound for φ are of size polynomial in the original SAT instance. If the encoding of Ref(φ) introduces super-polynomial blow-up, the hardness direction fails to establish NP-completeness.
minor comments (2)
  1. [Preliminaries] The precise definition and encoding of Ref(φ) should be stated with explicit clauses or an example early in the preliminaries to avoid ambiguity when discussing short refutations.
  2. [Main theorem statement] Clarify the quantitative meaning of 'short' or 'small' refutations (e.g., size bound relative to |φ|) in the statement of the main extraction theorem.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for the detailed referee report. We appreciate the positive assessment of the significance of our results. Below we provide point-by-point responses to the major comments. We will revise the manuscript accordingly to address the clarifications requested.

read point-by-point responses

  1. Referee: [PV1 formalization and extraction algorithm] The central extraction algorithm depends on the PV1 formalization supplying explicit poly-time witnessing functions for the non-existence of small refutations. The manuscript must clarify (in the section detailing the PV1 proof) that these witnesses are uniformly computable from an arbitrary Resolution derivation of ¬Ref(φ) in time polynomial in the refutation length, without size-dependent advice or oracles; otherwise the claimed polynomial-time procedure does not follow.

    Authors: We agree with this observation and will revise the manuscript to include the requested clarification. In the section describing the PV1 formalization of the Atserias-Müller lower bound, we will explicitly state that the witnessing functions provided by the PV1 proof are uniformly computable from any given Resolution derivation of ¬Ref(φ). The computation time is polynomial in the size of the derivation, and no size-dependent advice or oracles are required. This is a direct consequence of the feasible constructivity in PV1, ensuring the overall extraction algorithm runs in polynomial time. revision: yes

  2. Referee: [NP-completeness proof for PAP_EF] For the NP-completeness of PAP for EF, the reduction must ensure that both the constructed φ and the EF-proof of the Resolution lower bound for φ are of size polynomial in the original SAT instance. If the encoding of Ref(φ) introduces super-polynomial blow-up, the hardness direction fails to establish NP-completeness.

    Authors: We confirm that our reduction preserves polynomial sizes. The formula φ is constructed from the SAT instance in polynomial time, and the encoding of Ref(φ) has size polynomial in |φ| and the bit-length of the refutation size bound (which is logarithmic in the exponential bound but polynomial overall in the input). The EF-proof of the Resolution lower bound for φ is also of polynomial size, as it is built using the properties of the construction. To address the concern, we will add a dedicated paragraph analyzing the sizes of all components in the reduction to make this explicit. revision: yes

Circularity Check

0 steps flagged

New feasibly constructive proof of Atserias-Müller lower bound yields independent extraction algorithm

full rationale

The paper's central derivation supplies a polynomial-time extraction algorithm directly from a new feasibly constructive proof of the existing Atserias-Müller lower bound, formalized in PV1. This is a self-contained mathematical construction rather than any reduction of the output to fitted parameters, self-definitions, or load-bearing self-citations. The original 2020 lower bound is cited only for context while the constructive version and its PV1 formalization are developed here, with no equations or steps that equate the claimed prediction to its inputs by construction. The derivation remains independent of the present paper's own fitted values or prior results in a circular manner.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard axioms of bounded arithmetic (PV1) and the soundness/completeness properties of Resolution and Extended Frege; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • standard math Soundness and completeness of Resolution and Extended Frege proof systems
    Invoked when defining Ref(φ) and when stating that short refutations exist or do not exist.
  • domain assumption Formalizability of the Atserias-Müller lower bound inside PV1
    The extraction algorithm is claimed to follow from a feasibly constructive version formalizable in PV1.

pith-pipeline@v0.9.0 · 5921 in / 1501 out tokens · 53702 ms · 2026-05-22T00:41:49.421762+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

56 extracted references · 56 canonical work pages · 1 internal anchor

  1. [1]

    doi: 10.1016/j.ic.2003. 10.004. [AB09] S. Arora and B. Barak, Computational Complexity: A Modern Approach . Cambridge University Press,

    work page doi:10.1016/j.ic.2003 2003

  2. [2]

    Quantum automatingTC0-Frege is LWE-hard,

    doi: a10.1017/CBO9780511804090. [ACG24] N. Arteche, G. Carenini, and M. Gray, “Quantum automatingTC0-Frege is LWE-hard, ” in39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA , 2024, 15:1–15:25. doi: 10.4230/LIPIcs.CCC.2024.15. [AD08] A. Atserias and V. Dalmau, “A combinatorial characterization of resolution width, ”J...

    work page doi:10.4230/lipics.ccc.2024.15 2024

  3. [3]

    The complexity of the pigeonhole principle,

    doi: 10.1016/j.jcss.2007.06.025. [Ajt94] M. Ajtai, “The complexity of the pigeonhole principle, ”Combinatorica, vol. 14, no. 4, pp. 417– 433,

    work page doi:10.1016/j.jcss.2007.06.025 2007

  4. [4]

    From proof complexity to circuit complexity via interactive protocols,

    doi: 10.1007/BF01302964. [AKPS24] N. Arteche, E. Khaniki, J. Pich, and R. Santhanam, “From proof complexity to circuit complexity via interactive protocols, ” in51st International Colloquium on Automata, Languages, and Programming, 2024, Art. No. 12,

    work page doi:10.1007/bf01302964 2024

  5. [5]

    61 [All25] E

    doi: 10.4230/lipics.icalp.2024.12. 61 [All25] E. Allender, P-uniform vs. DLOGTIME-uniform AC0, Theoretical Computer Science Stack Exchange,

    work page doi:10.4230/lipics.icalp.2024.12 2024

  6. [6]

    Mean-payoff games and propositional proofs,

    doi: 10.4007/annals.2021.194.3.5. [AM11] A. Atserias and E. Maneva, “Mean-payoff games and propositional proofs, ” Inform. and Comput., vol. 209, no. 4, pp. 664–691,

    work page doi:10.4007/annals.2021.194.3.5 2021

  7. [7]

    Automating resolution isNP-hard,

    doi: 10.1016/j.ic.2011.01.003. [AM20] A. Atserias and M. Müller, “Automating resolution isNP-hard, ”Journal of the ACM (JACM) , vol. 67, no. 5, pp. 1–17,

    work page doi:10.1016/j.ic.2011.01.003 2011

  8. [8]

    Resolution is not automatizable unlessW[P] is tractable,

    doi: 10.1145/3409472. [AR08] M. Alekhnovich and A. A. Razborov, “Resolution is not automatizable unlessW[P] is tractable, ” SIAM Journal on Computing , vol. 38, no. 4, pp. 1347–1363,

    work page doi:10.1145/3409472

  9. [9]

    Feasibly constructive proof of Schwartz-Zippel lemma and the complexity of finding hitting sets,

    doi: doi:10.1137/06066850X. [AT24] A. Atserias and I. Tzameret, “Feasibly constructive proof of Schwartz-Zippel lemma and the complexity of finding hitting sets, ”Electronic Colloquium on Computational Complexity (ECCC), no. TR24-174,

    work page doi:10.1137/06066850x

  10. [10]

    The proof-search problem between bounded-width resolution and bounded- degree semi-algebraic proofs,

    [Online]. Available: https://eccc.weizmann.ac.il/report/2024/174/. [Ats13] A. Atserias, “The proof-search problem between bounded-width resolution and bounded- degree semi-algebraic proofs, ” inTheory and applications of satisfiability testing—SAT 2013 , ser. Lecture Notes in Comput. Sci. Vol. 7962, 2013, pp. 1–17.doi: 10.1007/978-3-642-39071-5\_1 . [BDG+...

    work page doi:10.1007/978-3-642-39071-5 2024

  11. [11]

    Simplified and improved resolution lower bounds,

    [Online]. Available: https://eccc. weizmann.ac.il/report/2020/105. [BP96] P. Beame and T. Pitassi, “Simplified and improved resolution lower bounds, ” inProceedings of 37th Conference on Foundations of Computer Science , 1996, pp. 274–282. doi: 10.1109/SFCS. 1996.548486. [BPR00] M. L. Bonet, T. Pitassi, and R. Raz, “On interpolation and automatization for...

    work page doi:10.1109/sfcs 2020

  12. [12]

    Parity games and propositional proofs,

    doi: 10.1137/S0097539798353230. [BPT14] A. Beckmann, P. Pudlák, and N. Thapen, “Parity games and propositional proofs, ”ACM Trans. Comput. Logic, vol. 15, no. 2, May

    work page doi:10.1137/s0097539798353230

  13. [13]

    [Bus86] S

    doi: 10.1145/2579822. [Bus86] S. R. Buss, Bounded arithmetic. Bibliopolis, Naples,

    work page doi:10.1145/2579822

  14. [14]

    Bounded arithmetic and propositional proof complexity,

    [Bus97] S. R. Buss, “Bounded arithmetic and propositional proof complexity, ” inLogic of computation (Marktoberdorf, 1995), ser. NATO Adv. Sci. Inst. Ser. F: Comput. Systems Sci. Vol. 157, Springer, Berlin, 1997, pp. 67–121. [Bus98] S. R. Buss, “First-order proof theory of arithmetic, ” inHandbook of proof theory, ser. Stud. Logic Found. Math. Vol. 137, N...

    work page doi:10.1016/s0049- 1995

  15. [15]

    Regular resolution effectively simulates resolution,

    doi: 10.1145/375827.375835. [BY24] S. Buss and E. Yolcu, “Regular resolution effectively simulates resolution, ”Inform. Process. Lett., vol. 186, Paper No. 106489, 4,

    work page doi:10.1145/375827.375835

  16. [16]

    Using the Groebner basis algorithm to find proofs of unsatisfiability,

    doi: 10.1016/j.ipl.2024.106489. 62 [CEI96] M. Clegg, J. Edmonds, and R. Impagliazzo, “Using the Groebner basis algorithm to find proofs of unsatisfiability, ” inProceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing (Philadelphia, PA,

    work page doi:10.1016/j.ipl.2024.106489 2024

  17. [17]

    The intrinsic computational difficulty of functions,

    , ACM, New York, 1996, pp. 174–183. doi: 10.1145/237814.237860. [Cob65] A. Cobham, “The intrinsic computational difficulty of functions, ” inLogic, Methodology and Philos. Sci. (Proc. 1964 Internat. Congr.) , North-Holland, Amsterdam, 1965, pp. 24–30. [Coo75] S. A. Cook, “Feasibly constructive proofs and the propositional calculus (preliminary ver- sion),...

    work page doi:10.1145/237814.237860 1996

  18. [18]

    A feasibly constructive lower bound for resolution proofs,

    , Association for Computing Machinery, New York, 1975, pp. 83–97. [CP90] S. Cook and T. Pitassi, “A feasibly constructive lower bound for resolution proofs, ”Information Processing Letters, vol. 34, no. 2, pp. 81–85,

    work page 1975

  19. [19]

    The relative efficiency of propositional proof systems,

    doi: 10.1016/0020-0190(90)90141-J. [CR79] S. A. Cook and R. A. Reckhow, “The relative efficiency of propositional proof systems, ”J. Symbolic Logic, vol. 44, no. 1, pp. 36–50,

    work page doi:10.1016/0020-0190(90)90141-j

  20. [20]

    On axiomatizability within a system,

    doi: 10.2307/2273702. [Cra53] W. Craig, “On axiomatizability within a system, ”J. Symbolic Logic, vol. 18, pp. 30–32,

    work page doi:10.2307/2273702

  21. [21]

    Automating algebraic proof systems isNP-hard,

    doi: 10.2307/2266324. [dRGN+21] S. F. de Rezende, M. Göös, J. Nordström, T. Pitassi, R. Robere, and D. Sokolov, “Automating algebraic proof systems isNP-hard, ” inProceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing , 2021, pp. 209–222. doi: 10.1145/3406325.3451080. [FFNR03] S. A. Fenner, L. Fortnow, A. V. Naik, and J. D. Rogers, “In...

    work page doi:10.2307/2266324 2021

  22. [22]

    Resolution lower bounds for refutation statements,

    doi: 10.1016/S0890-5401(03)00119-6. [Gar19] M. Garlík, “Resolution lower bounds for refutation statements, ” in44th International Sympo- sium on Mathematical Foundations of Computer Science , 2019, Art. No. 37,

    work page doi:10.1016/s0890-5401(03)00119-6 2019

  23. [23]

    Failure of feasible disjunction property for 𝑘-DNF resolution and NP-hardness of automating it,

    doi: 10.4230/ LIPIcs.MFCS.2019.37. [Gar24] M. Garlík, “Failure of feasible disjunction property for 𝑘-DNF resolution and NP-hardness of automating it, ” in39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, vol. 300, 2024, 33:1–33:23. doi: 10.4230/LIPIcs.CCC.2024.33. [Gay21] A. Gaysin, “H-coloring dichotomy in proof c...

    work page doi:10.4230/lipics.ccc.2024.33 2019

  24. [24]

    [Gay23] A

    doi: https://doi.org/10.1093/logcom/exab028. [Gay23] A. Gaysin, Proof complexity of CSP ,

    work page doi:10.1093/logcom/exab028

  25. [25]

    [Gay24] A

    arXiv: 2201.00913. [Gay24] A. Gaysin, Proof complexity of universal algebra in a CSP dichotomy proof ,

    work page arXiv

  26. [26]

    Automating cutting planes is NP-hard,

    [GKMP20] M. Göös, S. Koroth, I. Mertz, and T. Pitassi, “Automating cutting planes is NP-hard, ” in Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing , 2020, pp. 68–77. doi: 10.1145/3357713.3384248. [GL10] N. Galesi and M. Lauria, “On the automatizability of polynomial calculus, ”Theor. Comp. Sys., vol. 47, no. 2, pp. 491–506, Aug

    work page doi:10.1145/3357713.3384248 2020

  27. [27]

    On small-depth Frege proofs for PHP,

    doi: 10.1007/s00224-009-9195-5 . [Hås23] J. Håstad, “On small-depth Frege proofs for PHP, ” in2023 IEEE 64th Annual Symposium on Foundations of Computer Science—FOCS 2023 , IEEE Computer Soc., Los Alamitos, CA, 2023, pp. 37–49. doi: 10.1109/FOCS57990.2023.00010. 63 [HP11] L. Huang and T. Pitassi, “Automatizability and simple stochastic games, ” inAutomata...

    work page doi:10.1007/s00224-009-9195-5 2023

  28. [28]

    Automating OBDD proofs isNP-hard,

    doi: 10.1007/978-3-662-22156-3 . [IR22] D. Itsykson and A. Riazanov, “Automating OBDD proofs isNP-hard, ” in47th International Symposium on Mathematical Foundations of Computer Science (MFCS

    work page doi:10.1007/978-3-662-22156-3

  29. [29]

    Complexity of finding short resolution proofs,

    , vol. 241, 2022, 59:1–59:15. doi: 10.4230/LIPIcs.MFCS.2022.59. [Iwa97] K. Iwama, “Complexity of finding short resolution proofs, ” inMathematical foundations of computer science 1997 (Bratislava) , ser. Lecture Notes in Comput. Sci. Vol. 1295, Springer, Berlin, 1997, pp. 309–318. doi: 10.1007/BFb0029974. [Jeř05] E. Jeřábek, “Weak pigeonhole principle, an...

    work page doi:10.4230/lipics.mfcs.2022.59 2022

  30. [30]

    Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds,

    doi: 10.1017/jsl.2021.99. [Kha22b] E. Khaniki, “Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds, ” in37th Computational Complexity Conference (CCC

    work page doi:10.1017/jsl.2021.99 2021

  31. [31]

    Jump operators, interactive proofs and proof complexity generators,

    , ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 234, 2022, 17:1–17:15. doi: 10.4230/LIPIcs.CCC.2022.17. [Kha24] E. Khaniki, “Jump operators, interactive proofs and proof complexity generators, ” in2024 IEEE 65th Annual Symposium on Foundations of Computer Science (FOCS) , IEEE, 2024, pp. 573–593. [KM00] J. Köbler and J. Messner, “Is...

    work page doi:10.4230/lipics.ccc.2022.17 2022

  32. [32]

    Bounded arithmetic and the polynomial hierarchy,

    doi: 10.1006/inco.1997.2674. [KPT91] J. Krajíček, P. Pudlák, and G. Takeuti, “Bounded arithmetic and the polynomial hierarchy, ” Annals of Pure and Applied Logic, vol. 52, no. 1, pp. 143–153,

    work page doi:10.1006/inco.1997.2674 1997

  33. [33]

    On the weak pigeonhole principle,

    doi: 10.1002/rsa.3240070103. [Kra01] J. Krajíček, “On the weak pigeonhole principle, ”Fundamenta Mathematicae, vol. 170, no. 1-2, pp. 123–140,

    work page doi:10.1002/rsa.3240070103

  34. [34]

    [Kra19] J

    doi: 10.4064/fm170-1-8. [Kra19] J. Krajíček, Proof complexity. Cambridge University Press, Cambridge,

    work page doi:10.4064/fm170-1-8

  35. [35]

    A proof complexity conjecture and the incompleteness theorem,

    doi: 10.1017/jsl.2021.75. [Kra23] J. Krajíček, “A proof complexity conjecture and the incompleteness theorem, ”The Journal of Symbolic Logic, pp. 1–5,

    work page doi:10.1017/jsl.2021.75 2021

  36. [36]

    Extended Nullstellensatz proof systems,

    doi: 10.1017/jsl.2023.69. [Kra24] J. Krajíček, “Extended Nullstellensatz proof systems, ”Proceedings of the American Mathematical Society, vol. 152, pp. 4881–4892,

    work page doi:10.1017/jsl.2023.69 2023

  37. [37]

    64 [Kra25] J

    doi: doi.org/10.1090/proc/16709. 64 [Kra25] J. Krajíček, Proof Complexity Generators. Cambridge University Press, Cambridge,

    work page doi:10.1090/proc/16709

  38. [38]

    [Kra95] J

    doi: https://doi.org/10.1017/9781009611664. [Kra95] J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory . Cambridge Univer- sity Press, Cambridge,

    work page doi:10.1017/9781009611664

  39. [39]

    Metamathematics of Resolution lower bounds: A TFNP perspective,

    doi: 10.1017/CBO9780511529948. [LLR24] J. Li, Y. Li, and H. Ren, “Metamathematics of Resolution lower bounds: A TFNP perspective, ” Electronic Colloquium on Computational Complexity (ECCC) , no. TR24-190,

    work page doi:10.1017/cbo9780511529948

  40. [40]

    Feasibly constructive proofs of succinct weak circuit lower bounds,

    [Online]. Available: https://eccc.weizmann.ac.il/report/2024/190/. [MP20] M. Müller and J. Pich, “Feasibly constructive proofs of succinct weak circuit lower bounds, ” Annals of Pure and Applied Logic , vol. 171, no. 2, p. 102 735,

    work page 2024

  41. [41]

    Gap MCSP Is Not (Levin)NP-Complete in Obfustopia,

    doi: 10.1016/j.apal.2019. 102735. [MP24] N. Mazor and R. Pass, “Gap MCSP Is Not (Levin)NP-Complete in Obfustopia, ” in39th Computa- tional Complexity Conference (CCC 2024), ser. Leibniz International Proceedings in Informatics (LIPIcs), vol. 300, 2024, 36:1–36:21. doi: 10.4230/LIPIcs.CCC.2024.36. [MPW19] I. Mertz, T. Pitassi, and Y. Wei, “Short proofs are...

    work page doi:10.1016/j.apal.2019 2019

  42. [42]

    Typical forcings, NP search problems and an extension of a theorem of Riis,

    , vol. 132, 2019, 84:1–84:16. doi: 10.4230/LIPIcs.ICALP.2019.84. [Mül21] M. Müller, “Typical forcings, NP search problems and an extension of a theorem of Riis, ” Annals of Pure and Applied Logic , vol. 172, no. 4, p. 102 930,

    work page doi:10.4230/lipics.icalp.2019.84 2019

  43. [43]

    2020.102930

    doi: doi.org/10.1016/j.apal. 2020.102930. [Nar22] M. Narusevych, Models of bounded arithmetic and variants of pigeonhole principle ,

    work page doi:10.1016/j.apal 2020

  44. [44]

    [Nar24] M

    arXiv: 2208.14713. [Nar24] M. Narusevych, An independence of the MIN principle from the PHP principle ,

    work page arXiv

  45. [45]

    An independence of the MIN principle from the PHP principle

    arXiv: 2406.14930. [Oli25] I. C. Oliveira, “Meta-mathematics of computational complexity theory, ”Electronic Colloquium on Computational Complexity (ECCC) , no. TR25-041,

    work page internal anchor Pith review Pith/arXiv arXiv

  46. [46]

    Depth-𝑑 Frege systems are not automatable unless P = NP,

    [Online]. Available: https://eccc. weizmann.ac.il/report/2025/041/. [Pap24] T. Papamakarios, “Depth-𝑑 Frege systems are not automatable unless P = NP, ” in39th Computational Complexity Conference (CCC

    work page 2025

  47. [47]

    Exponential lower bounds for the pigeonhole principle,

    , vol. 300, 2024, 22:1–22:17. doi: 10.4230/ LIPIcs.CCC.2024.22. [PBI93] T. Pitassi, P. Beame, and R. Impagliazzo, “Exponential lower bounds for the pigeonhole principle, ”Computational Complexity, vol. 3, no. 2, pp. 97–140,

    work page 2024

  48. [48]

    A proof of the Kahn–Kalai conjecture,

    doi: 10.1007/BF01200117. [PP24] J. Park and H. T. Pham, “A proof of the Kahn–Kalai conjecture, ”J. Amer. Math. Soc., vol. 37, pp. 235–243,

    work page doi:10.1007/bf01200117

  49. [49]

    Learning algorithms versus automatability of Frege systems,

    doi: 10.1090/jams/1028. [PS22] J. Pich and R. Santhanam, “Learning algorithms versus automatability of Frege systems, ” in 49th International Colloquium on Automata, Languages, and Programming (ICALP

    work page doi:10.1090/jams/1028

  50. [50]

    229, 2022, 101:1–101:20

    , vol. 229, 2022, 101:1–101:20. doi: 10.4230/LIPIcs.ICALP.2022.101. [PS23] J. Pich and R. Santhanam, Towards P ≠ NP from Extended Frege lower bounds ,

    work page doi:10.4230/lipics.icalp.2022.101 2022

  51. [51]

    On reducibility and symmetry of disjoint NP pairs,

    arXiv: 2312.08163. [Pud03] P. Pudlák, “On reducibility and symmetry of disjoint NP pairs, ”Theoretical Computer Science, vol. 295, no. 1-3, pp. 323–339,

    work page arXiv

  52. [52]

    [Pud20] P

    doi: https://doi.org/10.1016/S0304-3975(02)00411-5. [Pud20] P. Pudlák,Reflection principles, propositional proof systems, and theories,

    work page doi:10.1016/s0304-3975(02)00411-5

  53. [53]

    Resolution lower bounds for perfect matching principles,

    arXiv:2007.14835. [Raz04] A. A. Razborov, “Resolution lower bounds for perfect matching principles, ”J. Comput. System Sci., vol. 69, no. 1, pp. 3–27,

    work page arXiv 2007

  54. [54]

    Bounded arithmetic and lower bounds in Boolean complexity,

    doi: 10.1016/j.jcss.2004.01.004. 65 [Raz95] A. A. Razborov, “Bounded arithmetic and lower bounds in Boolean complexity, ” inFeasible mathematics, II (Ithaca, NY,

    work page doi:10.1016/j.jcss.2004.01.004 2004

  55. [55]

    Iterated lower bound formulas: A diagonalization-based approach to proof complexity,

    , ser. Progr. Comput. Sci. Appl. Logic, vol. 13, Birkhäuser Boston, Boston, MA, 1995, pp. 344–386. [ST21] R. Santhanam and I. Tzameret, “Iterated lower bound formulas: A diagonalization-based approach to proof complexity, ” inProceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing , 2021, pp. 234–247. doi: https://dl.acm.org/doi/10.1145...

    work page doi:10.1145/3406325.3451010 1995

  56. [56]

    A Exponential approximation in PV1 Müller and Pich [MP20] formalized in PV1 the following useful bound

    doi: 10.4086/toc.2016.v012a005. A Exponential approximation in PV1 Müller and Pich [MP20] formalized in PV1 the following useful bound. Proposition A.1 ([MP20, Proposition 2.5]). Provably in PV1, for all 𝑛, 𝑚 ∈ Log such that 𝑛 < 𝑚, it holds that 1 − 𝑛/𝑚 ≤ 2−𝑛/𝑚. For our application in Lemma 6.3 we need to be able to take powers of this on both sides. Lemm...

    work page doi:10.4086/toc.2016.v012a005 2016