A Homological Proof of P != NP: Computational Topology via Categorical Framework

https://arxiv.org/abs/2510.17829

by rescrv • 9 months ago

12 21 9 months ago

arxiv.org

rescrv3• 9 months ago

I'm not sure if this is real, but the abstract says machine-verified.

krackers• 9 months ago

For a claim this big, I'm surprised only one author. Not even an advisor?

rescrv3• 9 months ago

Once upon a time, people published solo often. It's just harder to do things like that these days.

beanshadow• 9 months ago

Pg. 56 cites this repository which is either still private or doesn't exist:

https://github.com/comphomology/pvsnp-formal

seanhunter3• 9 months ago

Yes. From a quick scan of the paper, it includes a formal proof in Lean4. That said, it is very long and complicated, with lots of steps in the chain (as you might expect) so it would need to be checked carefully to ensure it proves what it claims to prove.

Lean uses Curry-Howard correspondence, so how proofs work is you declare your propositions as types and then your proof is actually a recipe that goes from things that have already been established and finishes by instantiating that type. The guarantees there are very strong - if you succeed in instantiating the type you have definitely proved something. The question is whether you have proved the thing you said you have. So here scanning the proof (it’s like 100 pages and I am sick so definitely sub-par intellectually) they use category theory to embed the problem, so the proof is actually a proof of the properties of this embedding. So if there is a problem with the proof, my guess would be that it would lie in the embedding not being exactly representative of the problem somehow.

It seems a pretty serious attempt though- it’s not just some random crank paper.

rescrv3• 9 months ago

Thank you! This is the kind of comment I hoped to see.

I'm betting it was published in a hurry. I know I would hit "publish" within 24 hours of creating such a result, and would hope it would go wide. I'd publish to arxiv before getting clearance to release the code. I bet that's what happened here.

I appreciate your explanation of the Curry-Howard correspondance. I was familiar with it, but not with Lean in particular. I'd heard of Lean, but didn't know how it worked.

Thank you again!

emtel• 9 months ago

The paper seems to make no mention of the natural proof barrier, so it is almost certainly not a proof of what it claims

soup102• 9 months ago

what's the natural proof barrier

seanhunter3• 9 months ago

Natural proofs are a certain type of proof of the circuit complexity of boolean conditions. The barrier is that it has been proved that [1] natural proofs cannot be used for P vs NP.

I’m not sure that is a problem here given that as I understand it, natural proofs apply to circuit complexity approaches and they say the whole circuit complexity method has fundamental limitations which they describe thus:

   The circuit complexity approach seeks to establish lower bounds by proving that NP problems require super-polynomial circuit sizes. While achieving success for restricted models such as monotone circuits, this approach has faced insurmountable barriers in establishing non-linear lower bounds for general circuits.

So they take an entirely different approach using category theory. It may have a similar limitation as the natural proof barrier (as far as I know), but as they dismiss the whole circuit idea and do something different I wouldn’t say them not mentioning the limitation of a specific type of circuit-based approach is that much of a problem.

[1] assuming certain things which people generally believe to be true

quamserena• 9 months ago

The GitHub repo 404’s and likewise with the Docker image. Where's the code?

https://github.com/comphomology/pvsnp-formal

steego• 9 months ago

The Github user doesn't even exist.

Who writes Lean code in the actual paper but doesn't create a repo or even a username?

goldsteinq• 9 months ago

Is this LLM-generated? The style is somewhat off (long lists repeating the same thing over and over, calling random meta statements “theorems”), and the link to the repo is completely broken.

nh23423fefe• 9 months ago

Every time I try to understand algebraic geometry I get stuck at just beyond varieties and ideals. I can't even work my way up to chain complexes and homologies to even get a hold on the content. Honestly functors and natural transformations, I dont grok either, so its greek to me.

Like whenever i'm working through definitions or content it all makes sense. But not being a working mathematician it all just blurs away into abstract nonsense that I can't organize internally.

orangea• 9 months ago

Learning homological algebra is a long way away from learning about varieties and ideals in any sensible order in which to learn material. You have to do a lot of work in between in order for homological algebra to seem motivated. Sounds like you ought to try an introduction to algebraic topology.

johncarlosbaez2• 9 months ago

You need to go more slowly and do lots of examples. Maybe start with

* Karen E. Smith, Lauri Kahanpää, Pekka Kekäläinen and William Traves, An Invitation to Algebraic Geometry, Springer, Berlin, 2004.

and then this:

* Igor R. Shafarevich, Basic Algebraic Geometry, two volumes, third edition, Springer, 2013.

il_abi• 9 months ago

math looks pretty legit. the only issue would come from the formulation of the category Comp and if it actually represents what it wants to. Hopefully some bigshot looks at this soon

yyyk• 9 months ago

The reddit people are very skeptical regarding the paper:

https://www.reddit.com/r/computerscience/comments/1odgx6v/le...

https://www.reddit.com/r/learnmath/comments/1odh3f5/is_this_...

johncarlosbaez2• 9 months ago

This claimed proof is a bunch of baloney:

* First, it's written in the typical style of AI slop.

* Second, a mathematician I know and trust writes "I went straight to the technical part (Sect. 3) and randomly checked one of the results (Theorem 3.14), finding that it is obviously false. (The category Comp mentioned in the theorem is formally introduced and makes sense per se, but it is certainly not additive with the proposed definition, as claimed in the statement of the theorem)."

* Third, another mathematician I know and trust writes "I spent almost an hour poking through here carefully to see where the more central claims begin to fall apart. Theorems 3.24 and 4.1 brazenly contradict each other, proving respectively that problems in P are homologically trivial and that all NP-complete problems are homologically isomorphic to all problems in NP. Even more to the point, the proof of 3.24 really shows the lie where it says "The detailed argument uses the functoriality of the computational homology construction and the fact that homology isomorphisms preserve the 'computational topology' of problems." The last claim is, naturally, not mathematically defined. The computational chain complex also appears not to be genuinely defined, as far as I can tell. I haven't compared to see what the author chucked into the formalized definition."

A Homological Proof of P != NP: Computational Topology via Categorical Framework

Related Stories