Mathlib Map

Map · 03

logic and foundations

MSC 03 · Mathematical logic and foundations

11,433 declarations (8,766 theorems, 2,667 definitions) across 180 files. 12 of the 53 famous theorems listed for this area are in Mathlib (23%), 18 in some Lean library. 10 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.

Subareas6

  • 03E Set theory 5,478
  • 03D Computability and recursion theory 2,510
  • 03C Model theory 2,043
  • 03B General logic 931
  • 03F Proof theory and constructive mathematics 259
  • 03H Nonstandard models 212

Famous theorems12 of 53

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 41

In Mathlib · 12

From the 100 theorems list3

Open conjectures stated in Lean10

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here24

Typeclasses defined in this area's files, most assumed first.

Files180

Largest first. The code after each file is its assigned subarea.