Optional: P is a proper subset of EXPTIME

Open

PvsNP.P_strictSubset_EXPTIME

by alexcarter · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryformalizationp-vs-np

P is a proper subset of deterministic exponential time, using the same TM2 framework and bounds two raised to a natural-coefficient polynomial in input length. This is a later sanity check, not a claim about NP.

Status: Known mathematics / implementation obligation awaiting formal proof.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem P_strictSubset_EXPTIME : P ⊂ EXPTIME := by sorry
end PvsNP

Source

Arora–Barak, Computational Complexity: A Modern Approach (2009); inspected author draft January 8, 2007, Definitions 1.4, 1.20, 2.1, 2.7, Claim 2.3, Theorem 2.6; https://theory.cs.princeton.edu/complexity/book.pdf; deterministic time hierarchy, Chapter 3; Sipser second edition Chapter 9. Exact-model simulation/hierarchy proof remains missing.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

The class $P$ is a proper subset of $EXPTIME$ : every language in $P$ lies in $EXPTIME$ , and the reverse inclusion fails, equivalently some language in $EXPTIME$ does not belong to $P$ . No hypotheses are supplied, and the time-bound definitions are exactly those expanded here. Here $B=\{\mathrm{false},\mathrm{true}\}$ , $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. The set $P$ consists exactly of languages $L\subseteq B^*$ for which there is a Boolean function $\chi:B^*\to B$ satisfying $D(\chi)$ and $\forall w\in B^*,\ w\in L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$ . Write $D(\chi)$ for existence of such a machine and a polynomial $p\in\mathbb N[X]$ that, for every $w\in B^*$ , compute the singleton output $[\chi(w)]$ from input $w$ in at most $p(|w|)$ steps. The set $EXPTIME$ consists exactly of languages $L\subseteq B^*$ for which there are a Boolean function $\chi:B^*\to B$ , a machine with a natural-valued time bound $t:\mathbb N\to\mathbb N$ computing $[\chi(w)]$ from $w$ within $t(|w|)$ steps for every $w$ , and $p\in\mathbb N[X]$ with $\forall n\in\mathbb N,\ t(n)\le 2^{p(n)}$ , such that $\forall w,\ w\in L\ \Longleftrightarrow\ \chi(w)=\mathrm{true}$ . The bound includes $n=0$ . A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. The supplied body is admitted with sorry; no proof of this assertion is supplied there.

View graph