P is closed under complement
ProvedPvsNP.coP_eq_P_tm2The class of languages whose complements belong to P equals P.
Status: Known mathematics / implementation obligation awaiting formal proof.
import Definitions.Def_PvsNPFrontier namespace PvsNP theorem coP_eq_P_tm2 : coP = P := by sorry end PvsNP
Read-back
What the Lean code literally says, in plain math · gpt-6-astra
The set of languages whose complements lie in equals : for every , if and only if . No additional hypothesis is present. Here , is the set of all finite Boolean lists, including the empty list, and is list length. The set consists exactly of languages for which there is a Boolean function satisfying and . Write for existence of such a machine and a polynomial that, for every , compute the singleton output from input in at most steps. 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.