Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

arxiv.org

Post reply on HN
Print view View original

11–20 of 22 posts

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

#11

Post by rescrv »

seanhunter wrote: post #9
rescrv wrote: post #2

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

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…

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!

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

#12

Post by seanhunter »

soup10 wrote: post #10
emtel wrote: post #6

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

what's the natural proof barrier

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

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

#13

Post by steego »

quamserena wrote: post #8

The GitHub repo 404’s and likewise with the Docker image. Where's the code? https://github.com/comphomology/pvsnp-formal

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?

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

#14

Post by soup10 »

seanhunter wrote: post #12
soup10 wrote: post #10

Earlier quoted context omitted.

what's the natural proof barrier

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 c…

i see, thanks

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

#15

Post by seanhunter »

rescrv wrote: post #11
seanhunter wrote: post #9

Earlier quoted context omitted.

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…

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 particul…

You are most welcome. Reading it a little more, the summary of the proof is they embed computations as a particular sort of category and then use homological algebra to show that computations in P have a certain property[1] and computations in NP have a different property[2], and they say they go on to demonstrate these properties are mutually incompatible, thus proving P != NP.

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)"

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

#17

Post by nh23423fefe »

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.

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

#18

Post by orangea »

nh23423fefe wrote: post #17

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…

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.

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

#20

Post by yyyk »

il_abi wrote: post #19

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

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_...

Post reply on HN