P versus NP, this project, and what is actually proved.

No. The current result is that P = NP is not established. The repository records five formal blockers, four project axioms, no eligible root theorem, and a closed publication gate.

P contains problems that can be solved efficiently. NP contains problems whose proposed answers can be checked efficiently. The question asks whether every efficiently checkable problem can also be solved efficiently.

The formal proof assistant Lean checks that each encoded proof step follows from its stated definitions, earlier theorems, and declared axioms. It does not make an unfinished argument complete, and it does not turn assumptions into proofs.

For arbitrary finite explicit BN4 cell ledgers, Lean now verifies a proof-bearing exact multiset embedding of the generated PkgC opposite-sign cancellation cells into an ambient ledger. The embedding preserves duplicate multiplicities and decomposes positive and negative mass at every complete key. Removing the balanced generated subledger leaves both the ambient signed mass and the executable residual signed contribution exactly equal to an explicit remainder. A successful candidate-derived BN4 kernel also proves that every embedded generated cell uses its canonical request-atom space, and complete bindings plus exact absence of every computed bridge imply V54 singletonization. The ambient ledger, typed restorer, exact permutation certificate or canonical serialization, and successful kernel remain proof-bearing inputs. Lean has not derived them from a terminal candidate, completed global route integration or silence, proved the full historical PkgC result, established polynomial runtime, ZeroSlack, PCCMin, SAT in P, removed a project assumption, or proved P = NP.

It is the current editorial estimate that 94% of the known formal reconstruction workload is complete. It is separate from the formal publication ledger, where 109 of 111 scoped rows are currently earned. Those rows are evidence gates of very different sizes, and the two unearned global rows contain many substantial obligations, so 109 divided by 111 is not the project completion percentage. The tracker is not a probability, confidence score, or claim that the overall route is correct, and it can decrease when new obligations are discovered.

They let readers identify the exact source and files being discussed and detect drift. A matching hash proves file identity only; it does not prove the mathematics inside the file.

Use the updates page or add the RSS/Atom feed to a feed reader. Each update has two plain-language paragraphs followed by a collapsed technical record.

Start at Technical review. It routes complexity theorists, Lean reviewers, and reproducibility reviewers to the report, formal status, architecture, source, and verification commands.