NP と coNP は等しいか？（短い反証は常に存在するか）

すべての恒真式に、その式の長さの多項式で収まる証明が存在するか。すなわち NP = coNP か否かを決定せよ。

Decide whether every tautology has a proof of length polynomial in the size of the tautology, equivalently whether NP = coNP.

Cook and Reckhow showed the question is equivalent to the existence of a polynomially bounded propositional proof system, which turned it into the research programme of proof complexity: prove superpolynomial lower bounds for stronger and stronger proof systems.

解決したかどうかは、問いではなくアプローチごとに決まります。Atlas は判定しません。外部の判定者が何をしたかを記録します。

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

  the Lean 4 typechecker, against the pinned toolchain · 型検査

  定式化

  NP != coNP, stated in Lean 4 over formalized complexity classes.問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The separation itself

  加えられた仮定・条件

  • The Lean encoding of the classes, as for P vs NP

  Statement only.

• Proof complexity lower bounds

  査読付きの証明

  到達状況

  進行中

  判定者

  the proof complexity community, through journal peer review · 査読

  定式化

  Prove superpolynomial lower bounds on proof length for propositional proof systems of increasing strength, up to a system strong enough to settle NP vs coNP.問いと同値

  保たれているもの

  • Exactly equivalent to the question, by the Cook-Reckhow programme

  弱まっているもの

  • Unconditional lower bounds exist only for weak systems (resolution, cutting planes); nothing is known for Frege and above

  加えられた仮定・条件

  • A ladder of proof systems that has to be climbed one rung at a time

  閉じた道

  • Feasible interpolation, the technique behind the known lower bounds for weak systems, provably fails for Frege systems under standard cryptographic assumptions; the ladder's next rung needs a different method.条件つき（standard cryptographic hardness assumptions）— 前提が崩れれば道は開く
    • paperdoi:10.1137/S0097539798353230M. Bonet, T. Pitassi, R. Raz, On interpolation and automatization for Frege systems, SIAM J. Comput. 29 (2000) 1939-1967: feasible interpolation fails for strong systems under cryptographic assumptions

  証拠

  • paperdoi:10.2307/2273702S. A. Cook, R. A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1979) 36-50: NP = coNP iff some propositional proof system is polynomially bounded

• Circuit lower bounds

  査読付きの証明

  到達状況

  進行中

  判定者

  the complexity theory community, through journal peer review · 査読

  定式化

  Prove a superpolynomial lower bound on the circuit size of an explicit function, which would give NP != coNP as a consequence.問いより強い

  保たれているもの

  • A lower bound of this kind settles the question outright

  加えられた仮定・条件

  • Proves a statement about all circuits, which is far stronger than the question needs

  Unconditional progress exists only for restricted circuit classes; Williams' NEXP vs ACC^0 is the high-water mark.

  閉じた道

  • Natural proofs: any lower-bound argument that is constructive and applies to a large fraction of functions would break the pseudorandom generators it assumes; almost every known technique is of this kind.条件つき（the existence of strong pseudorandom generators）— 前提が崩れれば道は開く
    • paperdoi:10.1006/jcss.1997.1494A. Razborov, S. Rudich, Natural proofs, J. Comput. System Sci. 55 (1997) 24-35
  • Relativization: there are oracles making the answer come out both ways, so no argument that survives adding an oracle can settle it.無条件
    • paperdoi:10.1137/0204037T. Baker, J. Gill, R. Solovay, Relativizations of the P =? NP question, SIAM J. Comput. 4 (1975) 431-442: oracles A, B with P^A = NP^A and P^B != NP^B
  • Algebrization: the natural algebraic extension of relativizing techniques is also insufficient, which rules out the arithmetization-based methods that beat relativization.無条件
    • paperdoi:10.1145/1490270.1490272S. Aaronson, A. Wigderson, Algebrization: a new barrier in complexity theory, ACM Trans. Comput. Theory 1 (2009), art. 2

  証拠

  • paperdoi:10.1145/2559903R. Williams, Nonuniform ACC circuit lower bounds, J. ACM 61 (2014), art. 2: NEXP is not contained in ACC^0

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Millennium/PvsNP.lean:48
• paperdoi:10.2307/2273702S. A. Cook, R. A. Reckhow, The relative efficiency of propositional proof systems, J. Symbolic Logic 44 (1979) 36-50: NP = coNP iff some propositional proof system is polynomially bounded

URI

https://atlasalt.com/q/be7b9e99-1128-4bfa-9856-528bdb146095

登録

2026-09-17

最終レビュー

2026-09-19

次回レビュー期限

2026-12-18

版

e4449428cdd6

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）