P と NP は等しいか？（P vs NP 問題）

解を多項式時間で検証できる問題は、すべて多項式時間で解けるか。すなわち P = NP か否かを決定せよ。

Decide whether every decision problem whose solutions are verifiable in polynomial time is also solvable in polynomial time.

One of the seven Clay Millennium Prize Problems, and the question against which the three named barriers of complexity theory (relativization, natural proofs, algebrization) were formulated.

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

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

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

  定式化

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

  保たれているもの

  • The separation itself

  加えられた仮定・条件

  • A particular Lean encoding of Turing machines and of the classes P and NP, whose agreement with the textbook definitions is itself a fidelity question

  Statement only. Formalizing complexity classes is delicate: the encoding, not the proof, is where the fidelity risk sits.

• 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 P != NP.問いより強い

  保たれているもの

  • 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

• Diagonalization

  閉じた道（障壁）

  到達状況

  この道では到達できないと証明済み

  判定者

  none: the obstruction is a published theorem · 引用

  差分（このアプローチが問いの何を保ち、何を弱めるか）はまだ書かれていません。人類審査で書きます。

  閉じた道

  • Baker, Gill and Solovay give oracles A and B with P^A = NP^A and P^B != NP^B. Any argument that relativizes therefore cannot settle the question, which rules out plain diagonalization.無条件
    • 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

• Geometric complexity theory

  査読付きの証明

  到達状況

  進行中

  判定者

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

  定式化

  Separate complexity classes by exhibiting representation-theoretic obstructions between orbit closures of the determinant and the padded permanent.問いより強い

  保たれているもの

  • Would separate the algebraic analogues, and the programme is explicitly aimed at P vs NP

  弱まっているもの

  • Targets the algebraic (VP vs VNP) statement first; the Boolean question does not follow automatically

  加えられた仮定・条件

  • Heavy machinery from algebraic geometry and representation theory

  閉じた道

  • Occurrence obstructions, the form of obstruction the programme originally proposed, provably do not exist for the determinant versus padded permanent problem.無条件
    • paperdoi:10.1090/jams/908P. Buergisser, C. Ikenmeyer, G. Panova, No occurrence obstructions in geometric complexity theory, J. Amer. Math. Soc. 32 (2019) 163-193

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Millennium/PvsNP.lean:40
• standardhttps://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdfS. Cook, The P versus NP problem, Clay Mathematics Institute official problem description

URI

https://atlasalt.com/q/43e24296-5a14-4cbc-b8ba-d9397a1a076d

登録

2026-09-17

最終レビュー

2026-09-19

次回レビュー期限

2026-12-18

版

ab1b05d3b2fc

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）