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.