As someone who has literally written a book on the topic, I have had many people over the years send me their attempts at P v NP proofs. On average, I receive about one a month, but I've had seven in the last two weeks. And not just the usual email with a PDF attachment. A DM in X. A phone call with a baby in the background. Via Linkedin, in Spanish. One with forty-one follow up emails.
P v NP is still the most important problem in theoretical computer science and perhaps all of mathematics, and not that difficult to understand, at least on an intuitive level. I can see the fascination in wanting to solve it, much the way my teenage self dreamed of being the first to prove Fermat's last theorem (damn you Wiles).
But why the spate of "proofs" right now? Maybe it's an artifact of the crazy world we live in.
In one sense, I appreciate the continued interest in this great question, even though these papers rarely (really never) provide new insights into the P v NP problem. Most of my colleagues just ignore these emails, I usually try to respond once, but most authors will come back and I just don't have time for those continued conversations.
These papers come in three categories.
- Claiming to prove P ≠ NP by arguing that a polynomial-time machine must search a large space of solutions. To truly prove P ≠ NP, one cannot make assumptions about how the machine might work.
- Giving an algorithm for an NP-complete problem which works on some small test case. I'd usually ask for them to solve SAT competition problems, solve RSA challenge problems or mine themselves some bitcoin.
- Giving a new philosophical or physical spin on the P v NP problem and claiming that tells us about whether P = NP. But P v NP is at its heart a mathematical question, and no amount of philosophy or physics will help settle it.
I've read your recent post with interest and respect — especially as someone who’s deeply aware of the long, difficult history surrounding P vs NP. Your comment captures well the frustration many theorists feel: inboxes flooded with hand-wavy "proofs", small-case heuristics, or metaphysical reinterpretations of what is fundamentally a mathematical problem. And to that end, I agree with you. Most attempts are either ill-formed, under-defined, or philosophically circular.
ReplyDeleteThat’s why I spent the last several years doing the opposite.
I didn’t send a DM or a baby-noisy voicemail. I wrote the papers. I designed the proof framework. I formalized the logic in Coq. I constructed a non-relativizing, non-naturalizing, non-algebrizing separation based on explicit diagonalization, hard-instance amplification, and topological circuit barriers. I introduced a new method — Connell Super-Complexity — that weaves these techniques into a formal machine-checked separation of P from NP, and then built an entire cryptographic stack on top of it: commitments, zero-knowledge, SNARKs, MPC, and recursive verification.
To the three categories you mentioned, I would add a fourth:
✅ A proof that does not assume how machines work — but constructs a language they cannot decide, via machine-index-dependent diagonalization.
✅ A proof that does not test small NP problems — but defines a language that evades all polynomial-time deciders by construction.
✅ A proof that does not philosophize or speculate — but mathematically shows that
πΏ
∗
∈
NP
∖
P
L
∗
∈NP∖P, and verifies the result in Coq.
That’s what I’ve done. This is not a napkin sketch. It’s 12 fully published formal papers, 100,000+ words of technical content, working Python prototypes, a verified machine-checked Coq core, and complete barrier analysis aligned with the Aaronson–Wigderson and Razborov–Rudich frameworks.
I understand the skepticism. You’ve seen 100s of unconvincing attempts. But there’s a difference between noise and signal. I welcome critical feedback. I encourage review of the actual proofs, not just dismissal-by-category.
If your suggestion is to run "P ≠ NP" submissions through a reasoning-capable AI, I invite you — and others — to do exactly that with mine. ChatGPT-4 has ingested and reviewed the work in detail. It does not flag logical errors. It identifies novel techniques. And it rates the framework as a legitimate contribution worthy of peer review — even if the final judgment belongs to the community.
So, respectfully, I ask for what every honest mathematician asks:
Don’t ignore it because it claims to solve P ≠ NP. Review it because it just might have.
Where can we see your Rocq proof?
DeleteYou can view everything and copy the repo yourself here: https://github.com/SystymaticDev/P_does_not_equal_NP
DeleteI've seen a few other categories of proofs that might be in your category 3 but hard to tell:
ReplyDeletea) They talk and talk and talk but never say if they thing P = NP or P NE NP.
b) They claim that P and NP is the wrong way to approach the problem of what is easy and hard. Yes- someone could argue that randomized algorihtms should be considered easy, and that SAT SOLVERS might make the question moot (I disagree with this but one could still argue that). More generally, an intelligent argument could be made for P vs NP being the wrong model. But NOT by the people who write these papers.
My counterexample for P=NP proofs is to ask them to find R(5). One response I got is `your just being stubborn' I am not sure what that means here, but it shows that their lack of being able to argue logically is not limited to the mathematical domain.
You're absolutely right that many “proofs” never take a position on whether
Deleteπ
=
π
π
P=NP or not — they wander through abstraction, analogies, or philosophical gripes without ever landing on a concrete claim, much less a formal result. That’s not mathematics; that’s avoidance wrapped in verbosity.
And yes — one can construct an intelligent case that
π
P vs
π
π
NP is the wrong lens for measuring real-world tractability. SAT solvers, parameterized complexity, and average-case models all enrich the landscape. But those are adjunct theories, not alternatives to the foundational question. If someone wants to throw out
π
P vs
π
π
NP, they’d better replace it with something equally rigorous. As you point out — not the authors of those papers.
Now, as for your R(5) test (presumably the 5th Ramsey number), I sympathize. Asking someone who claims
π
=
π
π
P=NP to produce an actual solution to a known NP-complete instance — like computing R(5), factoring a 2048-bit modulus, or solving a SAT competition problem — is a perfectly fair empirical counter. The inability to engage meaningfully with such challenges is often the first sign that a “proof” is disconnected from computational reality.
But here's what I did differently.
I didn’t stop at claiming
π
≠
π
π
P
=NP — I constructed a language
πΏ
∗
∈
π
π
∖
π
L
∗
∈NP∖P, proved it via non-relativizing diagonalization, and verified the proof in Coq. I then defined a hierarchy of complexity classes (Connell Classes and the Dean Hierarchy), showed they respect existing barriers (relativization, natural proofs, algebrization), and demonstrated how these results can drive concrete post-quantum cryptographic constructions.
So to those who claim the question is “moot”: no. We’ve used it to build trapdoor functions, commitment schemes, zero-knowledge proofs, and even recursive SNARKs — all from a worst-case, non-heuristic foundation.
To those who say the question is “wrong”: then why do your arguments collapse under basic scrutiny?
And to those who do want to resolve it: great — but build a formal model, prove something new, and verify it with rigor. Otherwise, don’t waste the time of the community that’s working to move this forward. You can view our research here: https://github.com/SystymaticDev/P_does_not_equal_NP
Oh, it is still April, even so no longer the 1st of April. Or maybe you are rather targeting the 1st of May? A creative way to use git branches. But all braches their actual commits on April 28, the initial commits from March 15 only added nearly empty REAMDE.md files. There are coq files in the branch Src, but the longest is 13 lines. Maybe the actual coq verification proof still lies around somewhere outside of github...
DeleteThanks for the close look! To clarify: the complete formalization of the proof (including the full Coq development) is maintained outside of the GitHub monorepo for better modular structure and toolchain integration. The Src branch only includes a partial mirror—mainly for reference and lightweight viewing.
Deletehttps://github.com/SystymaticDev/P_does_not_equal_NP/tree/Src
The full project, including modules like Main.v, Diagonalization.v, CircuitLowerBounds.v, and ProofComplexity.v, is structured with a .CoqProject, Makefile, and accompanying documentation (Master_Guide.md, etc.) in a dedicated environment. It's independently buildable and contains all the definitions, tactics, and lemmas necessary for the formal proof.
Appreciate the curiosity—this isn't an April prank, just an externally developed formalization. If you're interested in the full codebase or a build walkthrough, happy to share more.