Formal reconstruction in progress

A machine-checked reconstruction of a proposed route to P = NP.

Current result: P = NP is not established.

P versus NP asks whether problems with answers that can be checked efficiently can also be solved efficiently. Lean is software that checks each stated mathematical step. This project is rebuilding a proposed route in Lean so that completed steps, assumptions, and gaps are explicit.

Understand P versus NP View formal status

Latest machine-checked milestone

Lean now embeds finite PkgC cancellation into an ambient BN4 ledger

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. The 94% figure is a revisable editorial estimate, separate from the 109 of 111 scoped formal-publication rows and not a probability that the claim is correct.

Read the plain-language and technical update →

Technical theorem boundary · gate closed · 5 blockersnot established

Latest earned step: an exact multiset certificate embeds the generated balanced PkgC cancellation cells into an explicit ambient BN4 ledger. It preserves every duplicate and proves that removing the generated subledger leaves signed mass and executable residual contribution equal to an explicit remainder. Candidate-derived kernels retain canonical request atoms, and complete bindings with no computed bridge force V54 singletonization. The ambient ledger, restorer, certificate or serialization, and successful kernel remain inputs. This does not prove global PkgC route silence, global ZeroSlack, polynomial PCCMin, a target decider, a discharged axiom boundary, or P = NP.

status = "formal-reconstruction-in-progress"
mathematicalTheoremEstablished = false
publicTheoremEmissionAllowed = false
finalTheoremReady = false
rootLeanTheoremPresent = false
rootLeanTheoremBuilt = false
rootLeanTheoremAxiomAuditPassed = false
projectSpecificAxiomsRemaining = true
leanLockedNANDCarrierLayoutFormalized = true
leanLockedNANDCarrierTraceAxiomAuditPassed = true
leanLockedNANDCarrierTraceAuditedDeclarationCount = 71
leanLockedNANDGlobalCandidateAssemblyFormalized = true
leanLockedNANDGlobalCandidateAxiomAuditPassed = true
leanLockedNANDGlobalCandidateAuditedDeclarationCount = 71
leanLockedNANDGlobalBaselineDistinctFormalized = true
leanLockedNANDGlobalBaselineDistinctAxiomAuditPassed = true
leanLockedNANDGlobalBaselineDistinctAuditedDeclarationCount = 5
leanLockedNANDUnsatisfiableFinalZeroFormalized = true
leanLockedNANDUnsatisfiableFinalZeroAxiomAuditPassed = true
leanLockedNANDUnsatisfiableFinalZeroAuditedDeclarationCount = 2
leanLockedNANDGlobalSemanticThresholdFormalized = true
leanLockedNANDGlobalSemanticThresholdAxiomAuditPassed = true
leanLockedNANDGlobalSemanticThresholdAuditedDeclarationCount = 8
leanConcreteLockedNANDCanonicalEncodingFormalized = true
leanConcreteLockedNANDCompleteCandidateCodecFormalized = true
leanConcreteLockedNANDEncodedSemanticReductionFormalized = true
leanConcreteLockedNANDEncodedSemanticReductionAxiomAuditPassed = true
leanConcreteLockedNANDEncodedSemanticReductionAuditedDeclarationCount = 48
leanConcreteLockedNANDParserMachineFormalized = true
leanConcreteLockedNANDParserAxiomAuditPassed = true
leanConcreteLockedNANDParserAuditedDeclarationCount = 380
leanConcreteLockedNANDParserAllInputExactFormalized = true
leanConcreteLockedNANDParserExactOutputFormalized = true
leanConcreteLockedNANDParserCompiledNonTimeoutFormalized = true
leanConcreteLockedNANDParserPolynomialTimeMachineFormalized = true
leanConcreteLockedNANDParserPolynomialTimeFunctionFormalized = true
leanConcreteLockedNANDParserRawRefinementFormalized = true
leanConcreteLockedNANDEmitterMachineFormalized = true
leanConcreteLockedNANDEmitterAxiomAuditPassed = true
leanConcreteLockedNANDEmitterAuditedDeclarationCount = 3295
leanConcreteLockedNANDEmitterAllInputExactFormalized = true
leanConcreteLockedNANDEmitterExactTargetBytesFormalized = true
leanConcreteLockedNANDEmitterCompiledNonTimeoutFormalized = true
leanConcreteLockedNANDEmitterPolynomialTimeMachineFormalized = true
leanConcreteLockedNANDEmitterPolynomialTimeFunctionFormalized = true
leanConcreteLockedNANDEmitterRawRefinementFormalized = true
leanConcreteLockedNANDEmitterStrictParserCompositionFormalized = true
leanConcreteLockedNANDEmitterOutputSizeBoundFormalized = true
leanConcreteLockedNANDPolynomialReductionFormalized = true
leanConcreteCNFToNANDSemanticCompilerFormalized = true
leanConcreteCNFToNANDSemanticCompilerAuditedDeclarationCount = 68
leanConcreteCNFToNANDExactSemanticsFormalized = true
leanConcreteCNFToNANDPolynomialOutputSizeBoundFormalized = true
leanConcreteCNFToNANDAllBitstringFailClosedFormalized = true
leanConcreteCNFToNANDFiniteMachineFormalized = true
leanConcreteCNFToNANDPolynomialTimeFunctionFormalized = true
leanConcreteCNFToNANDPolynomialReductionFormalized = true
leanConcreteCNFToNANDPolynomialReductionAxiomAuditPassed = true
leanConcreteCNFToNANDPolynomialReductionAuditedDeclarationCount = 1316
leanConcreteCNFToNANDAllInputExactFormalized = true
leanConcreteCNFToNANDExactMachineOutputFormalized = true
leanConcreteCNFToNANDCompiledNonTimeoutFormalized = true
leanConcreteCNFToNANDRawRefinementFormalized = true
leanConcreteCNFToNANDDirectReductionFormalized = true
leanConcreteCNFToNANDLockedReductionCompositionFormalized = true
leanResidualGainChainVerifierFormalized = true
leanResidualGainChainAxiomAuditPassed = true
leanResidualGainChainSemanticInvariantFormalized = true
leanResidualGainChainSlackIterationBoundFormalized = true
leanLockedNANDGainIterationsAtMostFourFormalized = true
leanResidualGainChainPolynomialRuntimeFormalized = false
leanResidualGainStoppingSpecificationFormalized = true
leanResidualGainStoppingAxiomAuditPassed = true
leanResidualGainZeroIffGlobalNoStrictGainFormalized = true
leanResidualGainSemanticMinimumIffGlobalNoStrictGainFormalized = true
leanResidualGainChainGlobalStoppingConsequenceFormalized = true
leanResidualTerminalFullBridgeFormalized = true
leanResidualTerminalFullBridgeAxiomAuditPassed = true
leanResidualTerminalizationExactFormalized = true
leanResidualTerminalFullMinimumSpecificationFormalized = true
leanResidualTerminalMuBridgeFormalized = true
leanResidualWholeSpanPositiveWitnessIffFormalized = true
leanResidualWholeSpanStrictDescentFormalized = true
leanResidualWholeSpanZeroAbsenceIffFormalized = true
leanResidualTerminalQuotientCarrierFormalized = true
leanResidualTerminalModeFirewallFormalized = true
leanResidualProjectionMinimumAxiomAuditPassed = true
leanResidualProjectionMinimumExecutableFullScanFormalized = true
leanResidualProjectionMinimumExecutableQuotientScanFormalized = true
leanResidualProjectionMinimumMonotonicityFormalized = true
leanResidualProjectionDefectZeroIffCheckedLiftAtMinimumFormalized = true
leanResidualProjectionTransferFormalized = true
leanResidualProjectionTransferAxiomAuditPassed = true
leanResidualProjectionTransferSignedDeltasFormalized = true
leanResidualProjectionTransferIdentityFormalized = true
leanResidualProjectionTransferConstantCutFormalized = true
leanResidualTerminalProperSupportFormalized = true
leanResidualTerminalProperSupportSearchCompleteFormalized = true
leanResidualTerminalProperSupportExactLocalGainFormalized = true
leanResidualTerminalProperSupportAxiomAuditPassed = true
leanResidualTerminalProperSupportScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-and-canonical-primitive-record-seeds-with-exhaustive-reference-minimum-local-gain"
leanResidualTerminalSaturationFormalized = true
leanResidualTerminalSaturationAxiomAuditPassed = true
leanResidualTerminalPrimitiveUniverseFormalized = true
leanResidualTerminalSaturationExtensiveFormalized = true
leanResidualTerminalSaturationLeastFormalized = true
leanResidualTerminalSaturationMonotoneFormalized = true
leanResidualTerminalSaturationIdempotentFormalized = true
leanResidualTerminalExecutableSaturationFormalized = true
leanResidualTerminalPhysicalSupportCompletionFormalized = true
leanResidualTerminalPhysicalBoundaryFormalized = true
leanResidualTerminalPhysicalInterfaceFormalized = true
leanResidualTerminalPhysicalCompatibilityFormalized = true
leanResidualTerminalPhysicalSupportCompletionAxiomAuditPassed = true
leanResidualTerminalPhysicalSupportCompletionAuditedDeclarationCount = 35
leanResidualTerminalPhysicalSupportCompletionEmptyAxiomDeclarationCount = 8
leanResidualTerminalPhysicalSupportCompletionPropextOnlyDeclarationCount = 24
leanResidualTerminalPhysicalSupportCompletionPropextQuotSoundDeclarationCount = 3
leanResidualTerminalSupportExtractionFormalized = true
leanResidualTerminalOpenSemanticsFormalized = true
leanResidualTerminalInducedRecoveryFormalized = true
leanResidualTerminalSupportExtractionAxiomAuditPassed = true
leanResidualTerminalSupportExtractionAuditedDeclarationCount = 34
leanResidualTerminalSupportExtractionEmptyAxiomDeclarationCount = 3
leanResidualTerminalSupportExtractionPropextOnlyDeclarationCount = 11
leanResidualTerminalSupportExtractionPropextQuotSoundDeclarationCount = 20
leanResidualTerminalSupportCompletionFormalized = true
leanResidualTerminalSupportSquareClosureFormalized = true
leanResidualTerminalSupportSquareMeetJoinExactFormalized = true
leanResidualTerminalSupportSquarePhysicalCompatibilityFormalized = true
leanResidualTerminalSupportSquareSemanticExtractionFormalized = true
leanResidualTerminalSupportSquareClosureAxiomAuditPassed = true
leanResidualTerminalGovernedSupportCompletionFormalized = true
leanResidualTerminalGovernedProfilePartitionFormalized = true
leanResidualTerminalGovernedSupportCompletionAxiomAuditPassed = true
leanResidualTerminalFrontierPushoutFormalized = true
leanResidualTerminalFrontierBoundaryGlueExactFormalized = true
leanResidualTerminalFrontierInterfaceGlueExactFormalized = true
leanResidualTerminalFrontierProfileGlueExactFormalized = true
leanResidualTerminalFrontierInternalizationFormalized = true
leanResidualTerminalFrontierPushoutAxiomAuditPassed = true
leanResidualTerminalProjectionSquareFormalized = true
leanResidualTerminalProjectionPhysicalInvariantFormalized = true
leanResidualTerminalProjectionProfileExactFormalized = true
leanResidualTerminalProjectionMeetJoinCommuteFormalized = true
leanResidualTerminalProjectionPushoutCommuteFormalized = true
leanResidualTerminalProjectionSquareAxiomAuditPassed = true
leanResidualTerminalProjectionSquareScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-saturated-support-squares-and-forgetful-terminal-projections"
leanResidualTerminalSideTightMinimumArithmeticFormalized = true
leanResidualTerminalSideTightSignedSlackIdentityFormalized = true
leanResidualTerminalSideTightFailClosedGateFormalized = true
leanResidualTerminalSideTightCanonicalFullBasisFormalized = true
leanResidualTerminalSideTightCanonicalQuotientBasisFormalized = true
leanResidualTerminalSideTightMinimumAxiomAuditPassed = true
leanResidualTerminalSideTightMinimumScope = "all-finite-terminal-projection-four-corner-families-and-independently-attained-full-and-quotient-minimum-bases"
leanResidualTerminalFourCornerCarrierTransportFormalized = true
leanResidualTerminalFourCornerCarrierExactEndpointsFormalized = true
leanResidualTerminalFourCornerCarrierInjectiveCoordinatesFormalized = true
leanResidualTerminalFourCornerCarrierProfileTransportFormalized = true
leanResidualTerminalFourCornerCarrierFailClosedPhysicalTransportFormalized = true
leanResidualTerminalFourCornerCarrierAxiomAuditPassed = true
leanResidualTerminalFourCornerCarrierScope = "all-finite-computed-saturated-terminal-support-squares-and-canonical-physical-profile-transport-coordinates"
leanResidualTerminalFourCornerOptimaCarrierCompatibleFormalized = true
leanResidualTerminalFourCornerOptimaFaithfulAmbientizationFormalized = true
leanResidualTerminalFourCornerOptimaReferenceMinimumPreservedFormalized = true
leanResidualTerminalFourCornerOptimaLocalizedMinimaFormalized = true
leanResidualTerminalFourCornerOptimaSharedObserverProjectionFormalized = true
leanResidualTerminalFourCornerOptimaAxiomAuditPassed = true
leanResidualTerminalFourCornerOptimaCarrierScope = "all-finite-computed-saturated-terminal-support-squares-one-reversible-ambient-carrier-and-shared-observer-projection"
leanResidualTerminalFourCornerOptimumCoherenceClassifierFormalized = true
leanResidualTerminalFourCornerOptimumFirstFailureFormalized = true
leanResidualTerminalFourCornerOptimumRetainedSemanticsFormalized = true
leanResidualTerminalFourCornerOptimumProfileTransportFormalized = true
leanResidualTerminalFourCornerOptimumModeFirewallFormalized = true
leanResidualTerminalFourCornerOptimumSideTightTupleFactsFormalized = true
leanResidualTerminalFourCornerOptimumCoherenceAxiomAuditPassed = true
leanResidualTerminalFourCornerOptimumCoherenceScope = "all-finite-computed-terminal-support-squares-observers-projections-and-full-or-quotient-modes-coherent-tuple-or-deterministic-first-failure"
leanResidualTerminalFourCornerOptimumLocalRouteClassifierFormalized = true
leanResidualTerminalFourCornerOptimumRouteSoundnessFormalized = true
leanResidualTerminalFourCornerOptimumRouteSilenceFormalized = true
leanResidualTerminalFourCornerOptimumSideTightCompletionUnderRouteSilenceFormalized = true
leanResidualTerminalFourCornerOptimumExactCompletionValuesFormalized = true
leanResidualTerminalFourCornerOptimumPromotionFirewallRetained = true
leanResidualTerminalFourCornerSideTightCompletionAxiomAuditPassed = true
leanResidualTerminalFourCornerSideTightCompletionScope = "all-finite-computed-terminal-support-squares-observers-and-full-or-quotient-modes-side-tight-coherent-completion-under-exact-local-route-silence"
leanResidualTerminalFourCornerArbitraryFamilyCoherenceFormalized = true
leanResidualTerminalFourCornerExactMinimumFamilyEnumerated = true
leanResidualTerminalFourCornerTightBasisFamilyComplete = true
leanResidualTerminalFourCornerSignedTightBasisMaximumFormalized = true
leanResidualTerminalFourCornerTightBasisMaximumEqualsDeltaFormalized = true
leanResidualTerminalFourCornerTightBasisMaximumAxiomAuditPassed = true
leanResidualTerminalFourCornerTightBasisMaximumScope = "all-finite-computed-terminal-support-squares-observers-and-full-or-quotient-modes-complete-tight-basis-family-and-signed-maximum-under-exact-local-route-silence"
leanResidualTerminalCoherentFourCornerBasisFormalized = true
leanResidualTerminalCoherentFourCornerBasisScope = "conditional-on-exact-mode-appropriate-local-route-silence-not-universal-bn2-square-legitimacy"
leanResidualTerminalSquareLegitimacyFormalized = true
leanResidualTerminalSquareStructuralCompatibilityFormalized = true
leanResidualTerminalSquareFrontierPushoutFormalized = true
leanResidualTerminalSquareSharedQuantityCarrierFormalized = true
leanResidualTerminalSquareLocalConclusionUnderRouteSilenceFormalized = true
leanResidualTerminalSquareFailClosedRouteDichotomyFormalized = true
leanResidualTerminalSquareLegitimacyAxiomAuditPassed = true
leanResidualTerminalSquareLegitimacyScope = "all-finite-computed-terminal-support-squares-explicit-terminal-dependency-systems-direct-wire-candidates-observers-and-forgetful-projections-with-local-route-silence-or-proof-bearing-first-failure"
leanResidualTerminalComputedBCELAnchorNucleusFormalized = true
leanResidualTerminalBCELMinimumPositiveNucleusFormalized = true
leanResidualTerminalBCELAnchorAlgebraFormalized = true
leanResidualTerminalBCELCutDefectFirewallFormalized = true
leanResidualTerminalBCELCutRouteDichotomyFormalized = true
leanResidualTerminalBCELConstantCutConclusionFormalized = true
leanResidualTerminalBCELAnchorNucleusAxiomAuditPassed = true
leanResidualTerminalBCELAnchorNucleusScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-governed-proper-positive-supports-forgetful-projections-executable-ambient-observers-and-positive-whole-support-projection-defect"
leanResidualTerminalSaturationPositivityFirewallFormalized = true
leanResidualTerminalSaturationPositivityFirewallAxiomAuditPassed = true
leanResidualTerminalSaturationPositivityFirewallScope = "all-finite-direct-wire-candidates-explicit-terminal-dependency-systems-computed-governed-proper-positive-supports-forgetful-projections-and-executable-ambient-observers-total-zero-or-positive-whole-support-projection-defect-classification"
leanResidualTerminalCandidateSaturationFormalized = true
leanResidualTerminalSaturationCostBalanceFormalized = true
leanResidualTerminalFirstNontransparentStepFormalized = true
leanResidualTerminalSaturationCostBalanceAxiomAuditPassed = true
leanResidualTerminalSaturationCostBalanceScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-dependency-system-rule-labelled-exact-cost-balance-or-first-nontransparent-step"
leanResidualTerminalInterfaceExposureRoutingFormalized = true
leanResidualTerminalFiniteInterfaceExposureRoutesToEFormalized = true
leanResidualTerminalInterfaceExposureZeroCostRetractFormalized = true
leanResidualTerminalFirstInterfaceExposureRouteFormalized = true
leanResidualTerminalInterfaceExposureRoutingAxiomAuditPassed = true
leanResidualTerminalInterfaceExposureRoutingScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-interface-consumer-transparent-or-local-e-route-with-exact-first-failure"
leanResidualTerminalOriginKernelObligationRoutingFormalized = true
leanResidualTerminalFiniteOriginKernelObligationClosureRoutedFormalized = true
leanResidualTerminalFirstOriginKernelObligationRouteFormalized = true
leanResidualTerminalOriginKernelObligationRoutingAxiomAuditPassed = true
leanResidualTerminalOriginKernelObligationRoutingScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-candidate-derived-origin-kernel-obligation-closures-with-exact-safety-or-first-route"
leanResidualTerminalFiniteSaturatePositiveCompositionFormalized = true
leanResidualTerminalFiniteSaturatePositiveCompositionAxiomAuditPassed = true
leanResidualTerminalFiniteSaturatePositiveCompositionScope = "all-finite-direct-wire-candidates-executable-observers-forgetful-projections-proof-bearing-positive-full-slack-candidate-bcel-anchor-problems-total-finite-saturate-positive-composition"
leanResidualTerminalRankWFFormalized = true
leanResidualTerminalRankWFAxiomAuditPassed = true
leanResidualTerminalRankWFScope = "fixed-ten-coordinate-natural-lexicographic-order-executable-comparison-accessibility-induction-and-kernel-well-foundedness"
leanResidualTerminalBN3RequestEnvelopeFormalized = true
leanResidualTerminalBN3RequestEnvelopeAxiomAuditPassed = true
leanResidualTerminalBN3RequestEnvelopeScope = "successful-computed-finite-bcel-anchor-nuclei-canonical-stable-request-identities-exact-singleton-minimal-consumers-duplicate-free-incidence-and-jointly-side-tight-full-or-quotient-basis-family"
leanResidualTerminalBN4ActivationCancellationFormalized = true
leanResidualTerminalBN4ActivationCancellationAxiomAuditPassed = true
leanResidualTerminalBN4ActivationCancellationScope = "successful-computed-finite-bn3-envelope-explicit-typed-cell-ledgers-activation-exact-complete-key-same-key-cancellation-and-exact-integer-mass-residuals"
leanResidualTerminalBN5FullShadowLocalizationFormalized = true
leanResidualTerminalBN5FullShadowLocalizationAxiomAuditPassed = true
leanResidualTerminalBN5FullShadowLocalizationScope = "all-finite-exact-coordinate-negative-unit-refinements-computed-cut-silence-complete-multiplicity-coverage-or-strict-hall-deficit-with-local-x1-nonsilence"
leanResidualTerminalConsumerAntichainNormalFormFormalized = true
leanResidualTerminalConsumerAntichainNormalFormAxiomAuditPassed = true
leanResidualTerminalConsumerAntichainNormalFormScope = "all-finite-minimal-consumer-antichains-monotone-empty-false-nonzero-iff-disjoint-and-pkgc-singletonized-exact-v54-consumer-antichain-cut-indicator"
leanResidualTerminalConstantCutHypergraphRigidityFormalized = true
leanResidualTerminalConstantCutHypergraphRigidityAxiomAuditPassed = true
leanResidualTerminalConstantCutHypergraphRigidityScope = "all-finite-nonnegative-weighted-hypergraphs-constant-cut-hypergraph-rigidity-v53-q2-q3-q4-classification"
leanResidualTerminalBN6HypergraphPacketFormalized = true
leanResidualTerminalBN6HypergraphPacketAxiomAuditPassed = true
leanResidualTerminalBN6HypergraphPacketScope = "all-finite-explicit-grouped-v54-activation-to-v53-grouped-hypergraph-packet-bn6-pair-mixed-triple-fullspan-with-payload-witnesses"
leanResidualTerminalPkgCSeparatingConsumersFormalized = true
leanResidualTerminalPkgCSeparatingConsumersAxiomAuditPassed = true
leanResidualTerminalPkgCSeparatingConsumersScope = "all-finite-explicit-minimal-consumer-antichains-pkgc-separating-consumer-first-pair-canonical-atoms-exact-coordinate-restoration-or-strict-hall-local-q"
leanResidualTerminalPkgCTypedRestorationFormalized = true
leanResidualTerminalPkgCTypedRestorationAxiomAuditPassed = true
leanResidualTerminalPkgCTypedRestorationScope = "all-finite-explicit-minimal-consumer-antichains-typed-full-restoration-candidates-coordinate-preserving-exact-multiplicity-coverage-no-hall-or-singletonized"
leanResidualTerminalPkgCSameKeyCancellationFormalized = true
leanResidualTerminalPkgCSameKeyCancellationAxiomAuditPassed = true
leanResidualTerminalPkgCSameKeyCancellationScope = "all-finite-explicit-minimal-consumer-antichains-typed-exact-coordinate-restoration-canonical-opposite-sign-bn4-ledger-every-key-balanced-empty-residual-or-singletonized-under-cancellation-silence"
leanResidualTerminalPkgCAmbientBN4LedgerFormalized = true
leanResidualTerminalPkgCAmbientBN4LedgerAxiomAuditPassed = true
leanResidualTerminalPkgCAmbientBN4LedgerScope = "all-finite-explicit-ambient-bn4-ledgers-exact-multiset-embedding-balanced-generated-subledger-removal-preserves-remainder-signed-mass-and-candidate-derived-canonical-atom-linkage"
leanSaturatePositiveFormalized = false
leanBCELReadyFormalized = false
leanResidualRoutesGlobalGainCompletenessFormalized = false
leanZeroSlackCompletenessFormalized = false
leanPCCMinPolynomialRuntimeFormalized = false
concretePublicationGate.passed = false

Theorem emissionnot allowed

Root theoremnot present

Project axioms4 remain

Formal blockers5 active

Trust boundary: the current status is bound to the compiled Lean inventory. Hashes identify exact artefact bytes; they do not establish theorem correctness.

Source and release identifiers

Current inventoryPNP-LEAN-THEOREM-INVENTORY-2026-08-12-133

Current statusformal reconstruction

Inventory SHA-256696c76220a092e5a84e7caa804fd1c57889f193968d1285b520c408f8237f5c1

Coordinates and hashes make the published files identifiable and reproducible. They do not, by themselves, show that a mathematical statement is true.

The question in one minute

What does P versus NP ask?

Here, “efficiently” means the work grows at a manageable polynomial rate as the input gets larger. The question is foundational because it separates finding answers from checking them.

P: problems we can solve efficiently

There is an algorithm that finds an answer within the required polynomial-time limit.

NP: answers we can check efficiently

If someone supplies a proposed answer, an algorithm can verify it within a polynomial-time limit.

The open question

Does efficient checking always mean efficient solving? P = NP says yes. This project has not established that answer.

Choose your depth

Start where the language suits you.

The same status is presented at different levels; technical detail never replaces the plain statement of what is and is not proved.

New to P versus NP

Read short answers about the question, Lean, the current result, and what the percentage means.

Read the FAQ →

Following the project

See one everyday-language update for every newly earned formal milestone and subscribe by RSS.

Follow updates →

Auditing the technical work

Inspect the theorem boundary, formal report, architecture, source, hashes, and reproduction commands.

Open technical review →

Current bottom line

Machine checking now embeds the generated balanced PkgC cancellation cells into an explicit ambient BN4 ledger, but it has not derived that ledger or completed PkgC.

The new arbitrary-finite result accepts an exact proof-bearing multiset decomposition, preserves duplicate multiplicities, and leaves ambient signed mass and executable residual contribution equal to an explicit remainder. A successful candidate-derived kernel also retains canonical request atoms, and complete bindings with no computed bridge imply V54 singletonization. Deriving the ambient ledger, typed restorer, exact certificate, and successful kernel from terminal data, proving the restorer's semantic adequacy, full PkgC route silence, complete decreasing global routing, an efficient EncodedLockedNANDThreshold target solver, global ZeroSlack, polynomial PCCMin, and an eligible P = NP root theorem remain open.

See verified and missing work