Machine-Checked Formalization of Earlier Arguments on $\mathbb{P}$ versus $\mathbb{NP}$ Using Isabelle/HOL

Abstract

This letter revisits an earlier argument concerning $\mathbb{P}$ versus $\mathbb{NP}$ based on the SUBSET-SUM problem and examines its formalization in Isabelle/HOL. The formal development clarifies the argument's logical structure by separating its deductive combinatorial core from the broader universality principle required to extend it to all exact deterministic algorithms.

arXiv comment3 pages