Current findings and proof limits
Why a complete local search can still miss a global improvement
The project has verified a limit of the implemented circuit search: no fixed cap on the number of gates checked together makes it a complete test for global minimality. For every such cap, a circuit can be made smaller even though the complete bounded search finds no accepted improvement. Every proper selected part, including disconnected selections, is already minimal when its boundary inputs are treated as independent.
The result rules out using this fixed-size local search alone to certify that an entire circuit is minimal. It does not settle P versus NP or rule out growing windows or transformations that use the surrounding circuit. A corrected route must still prove global coverage and polynomial runtime for the complete construction. This correction does not earn a positive milestone or increase the proof-completion estimate.
This correction adds no earned positive publication row or fixed checkpoint credit. Read the verified correction and its limits.
A verified limit on replacing parts of a circuit
The project has verified a counterexample to an unrestricted reading of the original report's replacement claim. The checked example has a smaller replacement for one part, but inserting it would create a circular dependency; the whole circuit was already minimal.
This does not invalidate the checked replacement results that enforce the necessary restrictions, and it does not settle P versus NP. It identifies a central obligation for the next research: derive the admissible replacements and show that the general method can use them without losing the required saving.
This correction adds no earned positive publication row or fixed checkpoint credit. Read the verified correction and its limits.
Latest earned milestone: M280.
Proving cost comparisons for nested completed supports
For nested supports that have already been completed by the existing construction, the project now builds the comparison circuits needed to prove cost and positive-saving bounds. The bounds follow from those physical constructions instead of being assumptions.
This establishes the enlargement step for already-completed supports. It does not show that every raw local witness can be completed without losing its saving, and the complete admissibility and global routing arguments remain open.
This is not a globally successful rewrite strategy or a theorem of total polynomial runtime.
M230 and M231 retain the complete Cook-Levin builder and concrete CNF-SAT NP-completeness; a polynomial-time SAT decision algorithm remains open.
Risk-weighted proof completion estimate: 40%, with uncertainty 20% to 40%. Formal artefact coverage: 256 of 258 current scoped publication rows earned. Global gates closed: 0 of 5. Project-specific axioms remaining: 0. The eligible root theorem PNP.Main.p_eq_np remains absent and the publication gate is false.
P = NP is not established.
P versus NP, this project, and what is actually proved.
Short answers come first. Technical terms appear only where they help, with links to the exact formal status for readers who want to audit the work.
Does this project prove that P equals NP?
No. The current result is that P = NP is not established. The repository records five formal blockers, no project-specific axioms, no eligible root theorem, and a closed publication gate.
What is P versus NP?
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.
What does “machine-checked” mean?
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.
What did the latest milestone add?
For nested supports that have already been completed by the existing construction, the project now builds the comparison circuits needed to prove cost and positive-saving bounds. The bounds follow from those physical constructions instead of being assumptions.
This establishes the enlargement step for already-completed supports. It does not show that every raw local witness can be completed without losing its saving, and the complete admissibility and global routing arguments remain open.
Exact formal scope: For arbitrary finite wire carriers, keep masks and two raw seed lists whose computed completed supports are physically nested, derive the exact gate difference and crossing bindings. Extend the actual full or quotient reference minimum inside the common ambient input domain, preserving the larger padded ordinary interface and exact required computational-field availability, including false values. The derived comparisons prove that either minimum grows by at most the added physical gates, that full slack and support size minus quotient minimum are monotone, and that positive full slack or projection defect remains positive in the completed larger support. Raw-seed inclusion derives the physical inclusion. No cost inequality, field-equality certificate or optimizer is supplied to the final theorem.
Remaining boundary: This compares already completed dependency-closed supports in the computational-wire-profile model. It does not prove preservation of an arbitrary raw witness's initial positivity during completion, transparency of every intermediate event, monotonicity of projection defect alone, complete manuscript profile semantics, discovery of a proper positive support, global routing or unconditional SaturatePositive, BCELReady or ZeroSlack. Reference minimization, matching and influence computations remain exhaustive; complete polynomial PCCMin runtime, output-size and certificate bounds are not proved. The eligible root theorem remains absent and P = NP is not proved.
Why did the progress figure change from 98% to about 40%?
The earlier 98% figure was a narrower scoped-row/editorial measure that readers could too easily interpret as proof completion. The current formal artefact coverage is 256 of 258 scoped publication rows earned, or 99.2% of the current evidence ledger. Evidence rows are not equal units of mathematical difficulty, and the denominator can grow when dependencies are discovered or split into smaller rows.
The two remaining global publication rows aggregate five large proof blockers. Adding completed local submilestones can therefore make the old ratio approach 100% while none of those load-bearing gates closes. Historical mentions of 98% are retained as superseded scoped-row/editorial estimates, not current proof-completion claims.
The replacement is a fixed 100-point, risk-weighted checkpoint model. It currently awards 40 points, so the risk-weighted proof completion estimate is 40%, with an uncertainty range of 20% to 40%. It can move down as well as up if assumptions, hidden complexity, invalidated dependencies, or new blockers are found.
Neither 40% nor 99.2% is confidence that P=NP is true, the probability that the proposed route is correct, or an estimate of time remaining. See the five tracks and global gates or inspect the canonical machine-readable tracker.
Why publish reports, coordinates, and hashes?
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.
How can I follow new milestones?
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.
Where should a technical reviewer begin?
Start at Technical review. It routes complexity theorists, Lean reviewers, and reproducibility reviewers to the report, formal status, architecture, source, and verification commands.
A precise one-sentence description.
“PNP Labs is formally reconstructing a proposed route to P = NP in Lean; the repository does not currently establish the theorem.”