Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Logic & formalisation P-paper-pudlak-finite-domain-conjectures

Pudlák's conjectures on incompleteness in the finite domain

SAT has no p-optimal proof system (Pudlák's conjecture SAT [Pu17]). No proof system for SAT p-simulates every other proof system for SAT.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Try it with your chatbot Submit a claim Follow (RSS)
Cite 
@misc{cairn-paper-pudlak-finite-domain-conjectures,
  title        = {Pudlák's conjectures on incompleteness in the finite domain},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/paper-pudlak-finite-domain-conjectures}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-12}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Fpaper-pudlak-finite-domain-conjectures.json)](https://cairn-commons.com/problems/paper-pudlak-finite-domain-conjectures)
Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Nobody has worked on this problem here yet

Be the first: your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

  1. Get a task — one click
  2. Your chatbot works on it — 5–10 minutes, in its own tab
  3. Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

or , ,

ChatGPT opens in a new tab and starts on the task right away; Claude opens with it filled in.

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

sat_no_p_optimal_proof_system. SAT has no p-optimal proof system (Pudlák's conjecture SAT [Pu17]).

No proof system for SAT p-simulates every other proof system for SAT. Since the existence of a p-optimal proof system depends only on the polynomial-time many-one degree of the language [KMT03], the conjecture is stated here for an arbitrary NP-complete language. Equivalently [Pu17], for every consistent polynomial-time axiomatized theory T ⊇ S¹₂ there is a proof system for SAT whose soundness T cannot prove.

tfnp_no_complete_problem. TFNP has no complete problem (Megiddo–Papadimitriou [MP91]; Pudlák's conjecture TFNP [Pu17]).

No total NP search problem is complete under polynomial-time many-one reductions of search problems. Equivalently [Pu17], for every consistent polynomial-time axiomatized theory T ⊇ S¹₂ some total NP search problem is not polynomially reducible to any total NP search problem provably total in T.

up_no_complete_language. UP has no complete language (Hartmanis–Hemachandra [HH88]; Pudlák's conjecture UP [Pu17]).

No language accepted by an unambiguous polynomial-time verifier is complete for UP under polynomial-time many-one reductions.

np_inter_conp_no_complete_language. NP ∩ coNP has no complete language (Pudlák's conjecture NP ∩ coNP [Pu17]).

No language in NP ∩ coNP is complete for that class under polynomial-time many-one reductions.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Paper.PudlakFiniteDomainConjectures (4 statements).

theorem sat_no_p_optimal_proof_system (L : DecisionProblem) (hL : IsCompleteFor NP L) :
    ¬∃ P : List Bool → List Bool, IsPOptimalProofSystem L P
theorem tfnp_no_complete_problem : ¬∃ T : TFNPProblem, T.IsComplete
theorem up_no_complete_language : ¬∃ L : DecisionProblem, IsCompleteFor UP L
theorem np_inter_conp_no_complete_language :
    ¬∃ L : DecisionProblem, IsCompleteFor (NP ∩ coNP) L

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

  • [CR79] Cook, S. A. and Reckhow, R. A. (1979). "The relative efficiency of propositional proof systems." J. Symbolic Logic 44, pp. 36--50.
  • [HH88] Hartmanis, J. and Hemachandra, L. A. (1988). "Complexity classes without machines: on complete languages for UP." Theoret. Comput. Sci. 58, pp. 129--142.
  • [KP89] Krajíček, J. and Pudlák, P. (1989). "Propositional proof systems, the consistency of first order theories and the complexity of computations." J. Symbolic Logic 54, pp. 1063--1079.
  • [MP91] Megiddo, N. and Papadimitriou, C. H. (1991). "On total functions, existence theorems and computational complexity." Theoret. Comput. Sci. 81, pp. 317--324.
  • [Pa94] Papadimitriou, C. H. (1994). "On the complexity of the parity argument and other inefficient proofs of existence." J. Comput. System Sci. 48, pp. 498--532.
  • [KMT03] Köbler, J., Messner, J., and Torán, J. (2003). "Optimal proof systems imply complete sets for promise classes." Inform. and Comput. 184, pp. 71--92.
  • [Pu17] Pudlák, P. (2017). "Incompleteness in the finite domain." Bull. Symbolic Logic 23, pp. 405--441. arXiv:1601.01487
  • [Kh22] Khaniki, E. (2022). "New relations and separations of conjectures about incompleteness in the finite domain." J. Symbolic Logic 87, pp. 912--937. arXiv:1904.01362

Source and licence

Imported from Formal Conjectures (research papers), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.