Mathlib Map

Map · 14

algebraic geometry

MSC 14 · Algebraic geometry

8,207 declarations (6,370 theorems, 1,837 definitions) across 193 files. 1 of the 68 famous theorems listed for this area are in Mathlib (1%). 51 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.

Subareas11

  • 14A Foundations of algebraic geometry 6,142
  • 14H Curves in algebraic geometry 1,235
  • 14F (Co)homology theory in algebraic geometry 253
  • 14E Birational geometry 226
  • 14T Tropical geometry 118
  • 14L Algebraic groups 109
  • 14D Families, fibrations in algebraic geometry 67
  • 14M Special varieties 28
  • 14B Local theory in algebraic geometry 12
  • 14C Cycles and subschemes 9
  • 14P Real algebraic and real-analytic geometry 8

Famous theorems1 of 68

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

Not yet in Mathlib · 67

In Mathlib · 1

Open conjectures stated in Lean51

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here24

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

Files193

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