A Homological Proof of P != NP: Computational Topology via Categorical Framework (arxiv.org)

A single-author arXiv preprint claims a proof that P ≠ NP using a new “computational topology” framework and reports the proof has been fully formalized in Lean 4. The paper builds a category Comp that encodes problems and reductions, then attaches to each language L a chain complex C•(L) whose homology groups Hn(L) are proposed as topological invariants of computational processes. The core technical claim is that languages in P have trivial higher homology (Hn(L)=0 for n>0), while an NP-complete problem (SAT) has nontrivial homology (H1(SAT) ≠ 0), giving a homological separation between P and NP. The authors frame this as a categorical, homological analogue of structural complexity distinctions, and provide a Lean 4 formalization to back the arguments. If correct, this would resolve one of theoretical computer science’s central open problems and introduce homological algebra as a new tool for complexity theory, with downstream consequences for cryptography, reductions, and complexity classifications. That said, the claim is extraordinary and requires careful, independent vetting: formalization in Lean 4 increases confidence and reproducibility but does not substitute for community review of definitions, model assumptions, and reduction details. The paper’s technical innovations—Comp, the construction of C•(L), and the criteria linking homology to efficient computability—will be the focus of scrutiny and, if validated, could open a new research program using categorical and topological invariants to distinguish complexity classes.