A Homological Proof of P != Np: Computational Topology via Categorical Framework
Posted3 months agoActive2 months ago
arxiv.orgResearchstory
skepticalnegative
Debate
80/100
P vs NpComputational TopologyCategory Theory
Key topics
P vs Np
Computational Topology
Category Theory
A new arXiv paper claims to prove P != NP using homological methods, but the HN community is highly skeptical about its validity and the author's credentials.
Snapshot generated from the HN discussion
Discussion Activity
Active discussionFirst comment
N/A
Peak period
13
0-2h
Avg / period
2.6
Comment distribution21 data points
Loading chart...
Based on 21 loaded comments
Key moments
- 01Story posted
Oct 22, 2025 at 10:06 PM EDT
3 months ago
Step 01 - 02First comment
Oct 22, 2025 at 10:06 PM EDT
0s after posting
Step 02 - 03Peak activity
13 comments in 0-2h
Hottest window of the conversation
Step 03 - 04Latest activity
Oct 24, 2025 at 4:45 AM EDT
2 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
ID: 45677397Type: storyLast synced: 11/20/2025, 1:20:52 PM
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
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.
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!
I don't know homological algebra at all and only the very basics of category theory and while the (107-page) proof gives a lot of background it would take more time for me to get myself up to speed than I can really afford to spend right now. But that's the gist.
The fact that they have formalized the proof should mean it will be quicker to verify whether or not this is indeed it.
[1] which they call "contractible computational complexes (Hn(L) = 0 for all n > 0)."
[2] which they call "non-trivial homology (H1(SAT)̸ = 0)"
https://github.com/comphomology/pvsnp-formal
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:
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
https://github.com/comphomology/pvsnp-formal
Who writes Lean code in the actual paper but doesn't create a repo or even a username?
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.
* 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.
https://www.reddit.com/r/computerscience/comments/1odgx6v/le...
https://www.reddit.com/r/learnmath/comments/1odh3f5/is_this_...
* 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."