Map · 68
computer science
MSC 68 · Computer science
570 declarations (388 theorems, 182 definitions) across 9 files. 4 of the 33 famous theorems listed for this area are in Mathlib (12%). 13 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas2
- 68Q Theory of computing 426
- 68W Algorithms in computer science 144
Famous theorems4 of 33
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 29
In Mathlib · 4
- Akra–Bazzi theoremAkraBazziRecurrence.isBigO_asympBound
- Myhill–Nerode theoremLanguage.isRegular_iff_finite_range_leftQuotient
- Rice's theoremComputablePred.rice
- Smn theoremNat.Partrec.Code.smn
Open conjectures stated in Lean13
Statements without proofs, collected by the Formal Conjectures project.
- CernyConjecture.cerny_conjectureWikipedia
- ComplexityTheory.NP_ne_coNPMillennium Prize Problems
- ComplexityTheory.P_ne_NPMillennium Prize Problems
- PolyTime.isPolyTime_primeFactorsListWikipedia
- ScholzConjecture.scholz_conjectureWikipedia
Files9
Largest first. The code after each file is its assigned subarea.
- Mathlib.Computability.Language
Languages
68Q · 102
- Mathlib.Computability.AkraBazzi.SumTransform
Akra-Bazzi theorem: the sum transform
68W · 95
- Mathlib.Computability.ContextFreeGrammar
Context-Free Grammars
68Q · 94
- Mathlib.Computability.Encoding
Encodings
68Q · 81
- Mathlib.Computability.DFA
Deterministic Finite Automata
68Q · 71
- Mathlib.Computability.EpsilonNFA
Epsilon Nondeterministic Finite Automata
68Q · 64
- Mathlib.Computability.AkraBazzi.GrowsPolynomially
Akra-Bazzi theorem: the polynomial growth condition
68W · 32
- Mathlib.Computability.AkraBazzi.AkraBazzi
Divide-and-conquer recurrences and the Akra-Bazzi theorem
68W · 17
- Mathlib.Computability.MyhillNerode
Myhill–Nerode theorem
68Q · 14