Formalise the proposition P ≠NP

Stream: maths

[Mr Proof]

I haven't seen anywhere a formalisation of the proposition that P ≠NP. (Not the proof of it, just the statement). This seems the best place to ask.

Here is my attempt at the initial formalization (in psuedocode) . One part that is missing is just the statement of any NP problem such as the travelling salesman. I would be interested to hear if someone can improve this or point to the statement formalised somewhere else.

---

Let Alg(n) be a function that produces a solution S(n) to the travelling salesman of n-nodes T(n) in P(n) steps by repeated iteration. Let Proof(n) be a proof that Alg gives a solution S(n) in P(n) steps. 

Alg(n) can be represented by non-recursive function which is applied repeatedly, for P(n) steps:

Alg(n)(a_i) →a_i+1 

Alg(n) takes a constant time each step. After P(n) steps, the output is S(n).

The theorem states that P is non-polynomial:

∀(a:N,  ∃(m, ∀(m>n,  P(m)>m^a ))

(In the case where it can be less than that we can put in dummy instructions.). 

We also have Check(S,n) which is a function to check the solution which can be done in under a*n^c time for some a and c. CheckTS(S,n) can be a brute force check that the solution is the optimal one. Therefore if CheckTD(S(n),n) should be true if S(n) is the optimal a solution to T(n).

Therefor the statement of P vs NP  can be written as:

∀ (n:Nat)∀(data:Vec[n])∀(Alg:State →State),∀(P:Nat→Nat),

  CheckTS( Iterate( Alg(n),P(n) )Q(T(n)), n) →  ∀(a:N,  ∃(m, ∀(m>n,  P(m)>m^a ))

Q is a simple function to cast the travelling salesman initial data into a type that Alg can ingest.

Iterate is defined recursively as:

Iterate  f  (S n) x= f  (Iterate f n x)

Iterate  f  0 x = x

There may have to be some further restrictions on Alg to make sure it takes a constant time each step. Perhaps it has to be a Turing machine.**

---

Comments: Allowing an arbitrary function at each step in the algorithm is probably not valid since a function like 2^n would take exponential time to calculate in unary notation. So I'm still wondering what form Alg should take. Perhaps a Turing machine or a large matrix of size Q(n) where Q is some polynomial, acting on a large vector. It needs to be simple enough that it each step takes polynomial time (probably not provable inside Lean itself ?? ), but general enough that we can be convinced that it covers all algorithms without skipping over some "trick" that would make the algorithm polynomial.
Note: Since we are requiring it only takes P(n) steps, this means the Turing machine "tape" need only be of size I(n)+2P(n) where I(n) is the initial data, where we can pad it both sides. Also since Turing machines can be represented by large matrices, this is equivalent to saying that the algorithm is just found by M(n)^P(n) where M(n) is some large sparse matrix of size some function of n, acting on some vector of ones and zeros. So it might be possible to express this in terms of linear algebra.

[Mr Proof]

I have just seen this:

Which appears to be the statement of P ≠NP in Lean. (Although it may be unfinished?)

Is this generally accepted to be an accurate translation of the statement? Would anyone have time to explain it a bit?

[Martin Dvořák]

A few comments...

(1) If you write pseudocode, please, use the proper Lean syntax at least for function application and for quantifiers. Reading the pseudocode from your original post is painful.

(2) As you pointed out, the usual computational model is TM. We have Turing machines in Mathlib:
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean
However, the current formalization of TMs is sufficient only for developing Computability. A lot of work needs to be done before the TMs are viable for developing Complexity. It should be relatively easy to define the class P in the current framework. Defining the class NP will be a challenge. I strongly encourage you to do it and contribute it to Mathlib! However, before you start, you will need to study how things are done in Mathlib. The formalabstracts project is currently dead; I don't recommend building anything on top of it. At least until somebody starts developing fabstracts in Lean 4 in Mathlib-compatible way.

(3) Forget about Traveling Salesman Problem when formalizing the statement P vs NP. The statement must not assume results from the theory you want to formalize. Instead, it will later come as a theorem that P = NP iff TSP in P.

(4) You may want to have a look at the Cook-Levin paper in Isabelle/HOL by Frank Balbach. It contains much more than just the definitions, but you can ignore most of it.

[Bolton Bailey]

In particular, Turing.TM2ComputableInPolyTime is essentially a formalization of the class P. If you wanted to quickly get a formalization of a problem equivalent to P vs NP, you could take some known NP-Complete decision problem and ask if this structure could be constructed for it.

[Shreyas Srinivas]

I think you're setting yourself up for a world of pain if you start with the TM version of P vs NP. Have you looked at the descriptive complexity formulation?

[Shreyas Srinivas]

(deleted)

[Martin Dvořák]

Bolton Bailey said:

In particular, Turing.TM2ComputableInPolyTime is essentially a formalization of the class P.

I didn't know we already had P. Nice!

[Martin Dvořák]

Bolton Bailey said:

If you wanted to quickly get a formalization of a problem equivalent to P vs NP, you could take some known NP-Complete decision problem and ask if this structure could be constructed for it.

I don't like this part, as I pointed out above, but before we start arguing, it is important to answer the following question:

Do you literally want to state P vs NP in Lean? Or do you want to state a proposition that is known to be equivalent to P vs NP, where the part "known to be equivalent" stays on the informal level?

[Daniel Weber]

Shouldn't the certificate definition of NP be fairly trivial to formalize using P?

[Martin Dvořák]

Please try and do! I will be very happy if the definition of NP lands into Mathlib!

[Daniel Weber]

Why is docs#TM2OutputsInTime data?
Anyway, I tried something, but it's a mess. Does it look correct?

import Mathlib.Computability.TMComputable

open Computability Turing

def finEncodingListBool : Computability.FinEncoding (List Bool) where
  Γ := Bool
  encode := id
  decode := Option.some
  decode_encode _ := rfl
  ΓFin := inferInstance

@[simp]
lemma getLeft?_comp_inl {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
  ext
  simp

@[simp]
lemma getLeft?_comp_inr {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inl {α β : Type*} :
    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inr {α β : Type*} :
    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
  ext
  simp

@[simp]
lemma List.filterMap_none {α β : Type*} (l : List α) :
    l.filterMap (fun _ ↦ @Option.none β) = [] := by
  induction l <;> simp [*]

def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
    Computability.FinEncoding (α × β) where
  Γ := ea.Γ ⊕ eb.Γ
  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
      (eb.decode (x.filterMap Sum.getRight?))
  decode_encode x := by
    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
  ΓFin := inferInstance


structure NP {α : Type} (ea : FinEncoding α) (f : α → Prop) extends
    Turing.TM2ComputableAux (finEncodingPair ea finEncodingListBool).Γ
    finEncodingBoolBool.Γ where

  time : Polynomial ℕ

  /-- proof that this machine verifies `f` in at most `time(input.length)` steps -/
  outputsFun :
    ∀ a,
      f a ↔
      ∃ b : List Bool, Nonempty (TM2OutputsInTime tm
              (((finEncodingPair ea finEncodingListBool).encode (a, b)).map inputAlphabet.invFun)
              (.some (((finEncodingBoolBool.encode true).map outputAlphabet.invFun)))
              (time.eval (ea.encode a).length))

[Bolton Bailey]

Is it necessary to define a FinEncoding for List Bool? I would think that being mappable to List Bool is something close to what FinEncoding already means, so you could just go around it and let the witness type be arbitrary.

[Bolton Bailey]

Like this?

import Mathlib.Computability.TMComputable

open Computability Turing

@[simp]
lemma getLeft?_comp_inl {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
  ext
  simp

@[simp]
lemma getLeft?_comp_inr {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inl {α β : Type*} :
    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inr {α β : Type*} :
    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
  ext
  simp

@[simp]
lemma List.filterMap_none {α β : Type*} (l : List α) :
    l.filterMap (fun _ ↦ @Option.none β) = [] := by
  induction l <;> simp [*]

def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
    Computability.FinEncoding (α × β) where
  Γ := ea.Γ ⊕ eb.Γ
  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
      (eb.decode (x.filterMap Sum.getRight?))
  decode_encode x := by
    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
  ΓFin := inferInstance



structure TM2BoolComputableInNondeterministicTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β) (eBool : FinEncoding Bool)
  (f : α → Bool) extends TM2ComputableAux (finEncodingPair ea eb).Γ eBool.Γ where
  /-- a time function -/
  time : ℕ → ℕ
  /-- A function -/
  ndf : α × β → Bool
  /-- proof a machine outputs `ndf` in at most `time(input.length)` steps -/
  ndf_c : TM2ComputableInTime (finEncodingPair ea eb) eBool ndf
  /-- Proof the function computes f nondeterministically -/
  hf : ∀ a, (f a ↔ ∃ b, ndf ⟨a, b⟩)

[Bolton Bailey]

(Not sure that's right, it's confusing to me that TM2ComputableInTime isn't a predicate with the time function as an argument)

[Daniel Weber]

TM2ComputableInTime is a structure which contains the time inside it, so I don't think it's connected to your time function

[Daniel Weber]

Also I think the input in your input.length contains the certificate, which is wrong

[Bolton Bailey]

Ok let me try again:

import Mathlib.Computability.TMComputable

open Computability

namespace Turing

def isComputableInPolyTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β)
  (f : α → β) := ∃ _ : TM2ComputableInPolyTime ea eb f, true

def FinEncodingBool : FinEncoding Bool where
  Γ := Bool
  encode b := [b]
  decode l := l.head?
  decode_encode x := by simp
  ΓFin := Bool.fintype

@[simp]
lemma getLeft?_comp_inl {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
  ext
  simp

@[simp]
lemma getLeft?_comp_inr {α β : Type*} :
    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inl {α β : Type*} :
    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
  ext
  simp

@[simp]
lemma getRight?_comp_inr {α β : Type*} :
    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
  ext
  simp

@[simp]
lemma List.filterMap_none {α β : Type*} (l : List α) :
    l.filterMap (fun _ ↦ @Option.none β) = [] := by
  induction l <;> simp [*]

def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
    Computability.FinEncoding (α × β) where
  Γ := ea.Γ ⊕ eb.Γ
  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
      (eb.decode (x.filterMap Sum.getRight?))
  decode_encode x := by
    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
  ΓFin := inferInstance

def ComplexityClass (α : Type) := Set (α → Bool)

def P {α : Type} (ea : FinEncoding α) : ComplexityClass α :=
  { f | isComputableInPolyTime ea FinEncodingBool f }

def NP {α : Type} (ea : FinEncoding α) : ComplexityClass α  :=
  { f | ∃ β : Type, ∃ eb : FinEncoding β, ∃ p_wit : Polynomial ℕ,
          ∃ nf, isComputableInPolyTime (finEncodingPair ea eb) FinEncodingBool nf
                ∧ ∀ x, f x ↔ ∃ y, nf ⟨x, y⟩ ∧  (eb.encode y).length ≤ p_wit.eval (ea.encode x).length }

proof_wanted P_ne_NP {α : Type} (ea : FinEncoding α) : P ea ≠ NP ea

[Bolton Bailey]

(edited for the witness size problem)

[Daniel Weber]

FinEncodingBool already exists, docs#Computability.finEncodingBoolBool

[Jz Pan]

proof_wanted P_ne_NP {α : Type} (ea : FinEncoding α) : P ea ≠ NP ea

I think this is not true if α is a FinType

[Edward van de Meent]

right, because a function deciding if a condition holds for some finite number of elements can be completely memoised, and then will be linear.

[Bolton Bailey]

Update, I added an implementation of the conjecture to the deepmind conjectures repo here https://github.com/google-deepmind/formal-conjectures/pull/1120, I'd be interested if anyone could identify any issues with it.

[Bolton Bailey]

Also @Daniel Weber , I'd be interested to know if you're ok with me reusing the code you wrote above or whether I should just reimplement those encodings another way.

[Palalansoukî]

While it is not the standard way to formulate P ≠NP, using the representation of polynomial-time functions via safe functions, together with the fact that the quadratic Diophantine problem is NP-complete, yields an essentially equivalent and short formalization.

import Mathlib

namespace Nat

open Matrix

inductive SafeFunction : {n s : ℕ} → ((Fin n → ℕ) → (Fin s → ℕ) → ℕ) → Prop
  | zero : SafeFunction fun _ => 0
  | bit0 : SafeFunction fun (_ : Fin 0 → ℕ) (w : Fin 1 → ℕ) ↦ 2 * (w 0)
  | bit1 : SafeFunction fun (_ : Fin 0 → ℕ) (w : Fin 1 → ℕ) ↦ 2 * (w 0) + 1
  | div2 : SafeFunction fun (_ : Fin 0 → ℕ) (w : Fin 1 → ℕ) ↦ (w 0).div2
  | normal_proj (i : Fin n) : SafeFunction fun (v : Fin n → ℕ) (_ : Fin s → ℕ) ↦ v i
  | safe_proj (i : Fin s) : SafeFunction fun (_ : Fin n → ℕ) (w : Fin s → ℕ) ↦ w i
  | cond : SafeFunction fun (_ : Fin 0 → ℕ) (w : Fin 3 → ℕ) ↦ bif (w 0).bodd then w 1 else w 2
  | safe_comp
    {f : Fin n₂ → (Fin n₁ → ℕ) → (Fin 0 → ℕ) → ℕ}
    {g : Fin s₂ → (Fin n₁ → ℕ) → (Fin s₁ → ℕ) → ℕ}
    {h : (Fin n₂ → ℕ) → (Fin s₂ → ℕ) → ℕ}
    (hf : ∀ i, SafeFunction (f i))
    (hg : ∀ j, SafeFunction (g j))
    (hh : SafeFunction h) :
    SafeFunction fun (v : Fin n₁ → ℕ) (w : Fin s₁ → ℕ) ↦ h (fun i ↦ f i v ![]) (fun j ↦ g j v w)
  | safe_rec
    {f : (Fin n → ℕ) → (Fin s → ℕ) → ℕ}
    {g₀ : (Fin (n + 1) → ℕ) → (Fin (s + 1) → ℕ) → ℕ}
    {g₁ : (Fin (n + 1) → ℕ) → (Fin (s + 1) → ℕ) → ℕ}
    (hf : SafeFunction f)
    (hg₀ : SafeFunction g₀)
    (hg₁ : SafeFunction g₁) :
    SafeFunction fun (v : Fin (n + 1) → ℕ) (w : Fin s → ℕ) ↦
      (vecHead v).binaryRec (f (vecTail v) w) fun b k ih ↦ b.rec
        (g₀ (vecCons k (vecTail v)) (vecCons ih w))
        (g₁ (vecCons k (vecTail v)) (vecCons ih w))

abbrev PolyTimeComputable (f : (Fin n → ℕ) → ℕ) : Prop := SafeFunction fun v (_ : Fin 0 → ℕ) ↦ f v

def QDP : Set (ℕ × ℕ × ℕ) := {(a, b, c) | ∃ x y, a * x ^ 2 + b * y = c}

def PneNP : Prop := ¬∃ f : (Fin 3 → ℕ) → ℕ,
  PolyTimeComputable f ∧ ∀ a b c, (a, b, c) ∈ QDP ↔ f ![a, b, c] = 1

end Nat

[Daniel Weber]

Bolton Bailey said:

Also Daniel Weber , I'd be interested to know if you're ok with me reusing the code you wrote above or whether I should just reimplement those encodings another way.

Sure, feel free to use it

[Shreyas Srinivas]

I think while this is neat in terms of succinctness of formalising the conjecture, it is not going to be very helpful in verifying any candidate solutions. Like most problems in computer science this will have to be formulated in several equivalent ways (and there are a very large number of them).

[Shreyas Srinivas]

@Bolton Bailey’s formalisation is nice in this regard.

[Shreyas Srinivas]

Even here, I think a proper definition must include Karp and Turing reductions and a definition of NP Hardness and NP completeness.

[Palalansoukî]

I basically agree with your point, and I think that my approach is not suitable for formal-conjectures (since it is not the standard definition).
But the safe-function formalization is not just one of the numerous equivalent variant, it is better viewed as an alternative definition.

There are several ways to characterize computable functions, but Mathlib mainly uses the formalization by a function algebra with μ-minimization (Computable). There is also a Turing-machine version (Turing.TM2Computable), but it is not the primary usage when formalizing computability theory.

My method is also function algebra based, same style as Primrec, Partrec, and Computable, and we can define class P, NP, Karp reduction, etc.

abbrev PolyTimeComputable (f : (Fin n → ℕ) → ℕ) : Prop := SafeFunction fun v (_ : Fin 0 → ℕ) ↦ f v

def ClassP : Set (Set ℕ) :=
  {C | ∃ f, PolyTimeComputable f ∧ ∀ x, x ∈ C ↔ f ![x] = 1}

def ClassNP : Set (Set ℕ) :=
  {C | ∃ f, PolyTimeComputable f ∧ ∃ n, ∀ x, x ∈ C ↔ ∃ z, z.log2 ≤ x.log2 ^ n ∧ f ![x, z] = 1}

def KarpReducible (A B : Set ℕ) : Prop := ∃ f, PolyTimeComputable f ∧ ∀ x, x ∈ A ↔ f ![x] ∈ B

def PneNP : Prop := ClassP ≠ ClassNP

Moreover, because the definition is very simple, I believe that it can be more convenient than a TM-based one when formalizing actual proofs.