def
definition
currentStatus
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.PvsNPAssembly on GitHub at line 91.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
88 open_gap : String
89 sorry_count_in_chain : ℕ
90
91def currentStatus : PvsNPResolutionStatus where
92 conditional_proof_available := false
93 dissolution_proved := true
94 open_gap := "UniformTopologicalObstructionHyp: prove that for some fixed k, " ++
95 "every UNSAT formula on n variables requires circuits of size >= 2^(n/k)."
96 sorry_count_in_chain := 1
97
98/-! ## Master Certificate -/
99
100structure PvsNPMasterCert where
101 laplacian : JCostLaplacianCert
102 spectral : SpectralGapCert
103 frustration : JFrustrationCert
104 non_natural : NonNaturalnessCert
105 lower_bound : CircuitLowerBoundCert
106 dissolution : PvsNPDissolution
107 circuit_sep : CircuitSeparation
108
109def pvsNPMasterCert : PvsNPMasterCert where
110 laplacian := jcostLaplacianCert
111 spectral := spectralGapCert
112 frustration := jfrustrationCert
113 non_natural := nonNaturalnessCert
114 lower_bound := circuitLowerBoundCert
115 dissolution := dissolution_holds
116 circuit_sep := circuitSeparation
117
118end -- noncomputable section
119
120end PvsNPAssembly
121end Complexity