Potential projects

This is a rough list (initially inspired by the Orsay meeting) of mathematics that we'd like to see in Lean, and that should be not-too-hard from where we are now.

Maybe a good workflow is something like: idea -> this list -> coding -> write documentation -> PR to mathlib?

Analysis

• trigonometric functions, π (see also) (major progress by Chris)
• integrals on measure spaces
• Bochner integrals
• Fréchet derivatives
• Stone-Weierstrass
• smooth manifolds

Linear algebra

• finite dimensional vector spaces (UROP)
• matrices (work done by Ellen Arlt here)
  • links to linear maps (work done by Blair Shi and Keji Neri here)
  • determinant and trace (work done by Keji Neri here)
  • Cayley--Hamilton
  • Gaussian elimination
• tensor and exterior algebra (note Kenny Lau's work on tensor products)
• classification of quadratic forms by signature
• Ellenberg-Gijswijt (Johannes)

Galois theory

• field homomorphisms are injective
• splitting fields (community)
• finite fields
  • e.g. as splitting fields for x^(p^k) - x
• finite extensions

Number theory

• Quadratic reciprocity (Chris) (this has been PR'ed!)
• Number fields (waiting for module refactoring)
• Adeles (see former issue)

Commutative algebra

• PIDs (definition is in mathlib, by Chris)
• Smith normal form (do Gaussian elimination first!) and the structure theorem for modules over a PID
• Noetherian rings
  • Noetherian modules over Noetherian rings (community)
  • Hilbert basis theorem (Kevin; waiting for module refactoring)
• Perfectoid spaces (needs Noetherian rings plus Patrick/Johannes's work on completions and plenty more).

Category theory

• limits/colimits (Scott)
• sheaves (being actively worked on by Bhavik)
• enriched categories
• 'concrete' categories
• adjunctions

Algebraic topology

• connectedness (UROP -- see connected_spaces, path_connectedness and local_connectedness files)
• fundamental groups (higher homotopy groups?) (UROP, Reid)
• singular/cellular/... homology (Johan)
• Brouwer fixed point theorem
• Eilenberg–Steenrod axioms
• suspensions, mapping spaces, loop spaces
• O(n) is homotopy equivalent to GL(n)

Longer term

• some representation theory?
• some Lie theory?
• simplicial sets are a model category
• Bott periodicity
• https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean