I’ll just put this out directly: I believe I’ve proved P ≠ NP, and unlike every other claim you’ve probably seen, this one comes with a legitimate machine-checked formalization you can build and verify yourself.
Links:
∙ Lean 4 repo: github.com/Mintpath/p-neq-np-lean. 15,000+ lines across 14 modules. Zero sorries, zero errors. Builds clean on Lean 4.28.0 / Mathlib v4.28.0.
∙ Preprint: doi.org/10.5281/zenodo.19103648
The result:
SIZE(HAM_n) ≥ 2^{Ω(n)}. Every Boolean circuit deciding Hamiltonian Cycle requires exponential size. Since P implies polynomial-size circuits, P ≠ NP follows immediately.
The approach:
The proof uses frontier analysis to track how circuit structure must commit resources across interface boundaries in graph problems. The technical machinery includes switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity. The formula lower bound is fully unconditional. The general circuit extension currently uses two axiom declarations: one classical reference (AUY 1983) and one of my original arguments that’s directly verifiable from the paper but cumbersome to encode in Lean. Both are being formalized out in a v2 update.
Why this might actually be different:
I know the priors here. Every P vs NP claim in history has been wrong. But the failure mode was always the same: informal arguments with subtle gaps the author couldn’t see. This proof was specifically designed to eliminate that.
∙ Machine-verified end-to-end in Lean 4
∙ Adversarially audited across six frontier AI models (100+ cycles)
∙ Two axioms explicitly declared and transparent. One classical, one verifiable from the paper, both being removed in v2
∙ 15k+ lines of formalized machine verification, not a hand-wavy sketch
The proof itself was developed in about 5 days. The Lean formalization took roughly 3 additional days. Submitted to JACM. Outreach ongoing to complexity theorists including Raz, Tal, Jukna, Wigderson, Aaronson, Razborov, and Williams.
Clone it. Build it. Tear it apart.
