Mathlib reviewers

Members

• Aaron Anderson (@awainverse) t-logic t-combinatorics

  model theory

• Adam Topaz (@adamtopaz) t-algebraic-geometry t-category-theory t-meta t-number-theory t-ring-theory
• Alex J. Best (@alexjbest) t-number-theory t-algebraic-geometry t-meta

  Not super active reviewing right now but I can be tempted occasionally going forward

• Anatole Dedecker (@ADedecker) t-analysis t-dynamics t-geometric-group-theory t-topology

  topology, functional analysis, calculus

• Andrew Yang (@erdOne) t-algebra t-algebraic-geometry t-category-theory t-ring-theory

  commutative algebra

• Anne Baanen (@Vierkantor) t-algebra t-data t-meta t-number-theory t-order tech debt documentation

  Typeclasses, hierarchies, optimization and refactoring, metaprogramming, lattices (order theory)

• Bhavik Mehta (@b-mehta) t-category-theory t-combinatorics t-set-theory
• Bryan Gin-ge Chen (@bryangingechen) CI t-order
• Christian Merten (@chrisflav) t-algebra t-ring-theory t-algebraic-geometry
• Dagur Asgeirsson (@dagurtomas) t-algebra t-algebraic-geometry t-algebraic-topology t-category-theory t-condensed t-topology

  t-algebra and t-topology include everything in Algebra/Category, Algebra/Homology, Topology/Category and more, but not everything with these labels.

• Damiano Testa (@adomani) t-algebra t-linter

  metaprogramming (because I like it, not because I feel that I am very skilled in it!)

• David Loeffler (@loefflerd) t-number-theory

  Algebraic and analytic number theory; also topology, real analysis, Fourier theory

• David Renshaw (@dwrensha) t-meta IMO
• Eric Rodriguez Boidi (@ericrbg) t-algebra t-computability t-data t-logic t-number-theory t-set-theory

  sorry for the late reply - happy to review every so often. will try and get back into reviewing a little more!

• Eric Wieser (@eric-wieser) t-algebra t-data t-euclidean-geometry t-meta

  algebra, infrastructure

• Etienne Marion (@EtienneC30) t-measure-probability

  mostly interested in probability theory and statistics

• Filippo A. E. Nuccio (@faenuccio) t-group-theory t-functional-analysis t-ring-theory

  Functional Analysis, General Topology (because I like them a lot without being an expert)

• Floris van Doorn (@fpvandoorn) t-analysis t-differential-geometry t-logic t-topology

  maybe metaprogramming

• Frédéric Dupuis (@dupuisf)
• Gabriel Ebner (@gebner)
• Heather Macbeth (@hrmacbeth) t-differential-geometry t-analysis

  geometry, analysis

• Jireh Loreaux (@j-loreaux) t-analysis t-topology
• Johan Commelin (@jcommelin) CI t-algebra t-algebraic-geometry t-algebraic-topology t-category-theory t-condensed t-group-theory t-number-theory t-ring-theory t-topology tech debt

  hierarchies, generic maintenance

• Jon Eugster (@joneugster) CI t-algebra t-algebraic-geometry t-condensed t-data t-linter t-meta t-ring-theory tech debt

  priority on t-meta, t-linter, CI

• Joseph Myers (@jsm28) IMO t-euclidean-geometry
• Jovan Gerbscheid (@JovanGerb) t-linter t-meta tech debt

  tactics; core features such as unification, type class search and simp; performance improvements (in the above); elaboration/delaboration

• Joël Riou (@joelriou) t-category-theory t-algebra t-algebraic-geometry t-algebraic-topology
• Julia Markus Himmel (@TwoFX) t-data

  I am also knowledgeable about much of the category theory library. I don't have time right now do to many reviews in category theory, but feel free to request reviews for specific category theory PRs from me.

• Junyan Xu (@alreadydone) t-algebra t-algebraic-geometry t-number-theory t-ring-theory t-topology t-set-theory
• Kevin Buzzard (@kbuzzard) t-number-theory t-algebra t-ring-theory
• Kexing Ying (@kex-y) t-measure-probability

  Stochastic processes

• Kim Morrison (@kim-em) t-meta t-category-theory t-algebra t-algebraic-geometry
• Kyle Miller (@kmill) t-meta t-combinatorics
• Mario Carneiro (@digama0) t-computability t-meta

  lean formalization, tactics, type theory, proof engineering

• María Inés de Frutos-Fernández (@mariainesdff) t-algebra t-number-theory t-ring-theory
• Matthew Robert Ballard (@mattrobball) t-category-theory t-algebra t-algebraic-geometry t-algebraic-topology t-group-theory t-ring-theory

  Folders in mathlib: Algebra, AlgebraicGeometry, AlgebraicTopology, CategoryTheory, Data, FieldTheory, Geometry, GroupTheory, Lean, LinearAlgebra, NumberTheory, RepresentationTheory, RingTheory, Tactic, Topology, Util

• Michael Rothgang (@grunweg) t-differential-geometry t-analysis t-topology t-linter tech debt
• Michael Stoll (@MichaelStollBayreuth) t-number-theory

  more algebraic than analytic number theory

• Miyahara Kō (@Komyyy) t-computability t-order

  While there are a fairly wide range of Mathlib topics I'm knowledgeable about, since I'm new and not yet fully comfortable with the process, I would like to register only the following two as my preferences on the queueboard:

  • t-computability
    • Because I'm planning to complete the formalization of Matiyasevich's theorem(s is Diophantine ↔ s isrecursive enumerable), which is currently still in progress
  • t-order
    • Because I am familiar with Filter
• Monica Omar (@themathqueen) t-algebra t-analysis

  operator algebras

• Moritz Doll (@mcdoll) t-analysis t-dynamics t-topology
• Oliver Nash (@ocfnash) t-algebra t-topology t-differential-geometry
• Patrick Massot (@PatrickMassot) t-topology t-differential-geometry
• Reid Barton (@rwbarton)
• Riccardo Brasca (@riccardobrasca) t-algebra t-algebraic-geometry t-category-theory t-condensed t-group-theory t-number-theory t-ring-theory
• Robert Y. Lewis (@robertylewis) t-meta CI
• Robin Carlier (@robin-carlier) t-algebraic-topology t-category-theory

  I’m mainly interested in things around category theory, especially things with higher-categorical/homotopical flavors. Most familiar with the CategoryTheory/ stuff, and stuff in AlgebraicTopology that deals with simplicial sets/simplicial objects.

• Ruben Van de Velde (@Ruben-VandeVelde)

  Interest- probably anything related to flt Competence- mostly undergrad stuff / refactoring

• Rémy Degenne (@RemyDegenne) t-measure-probability
• Simon Hudon (@cipher1024)
• Sébastien Gouëzel (@sgouezel) t-measure-probability t-analysis t-differential-geometry t-dynamics
• Thomas Browning (@tb65536) t-group-theory t-number-theory
• Thomas R. Murrills (@thorimur) t-linter t-meta

  Primarily focused on metaprogramming!

• Yakov Pechersky (@pechersky) t-algebra t-data t-order

  discrete math, fin and fintype, bundled ordered algebraic structures, p-adic fields and nonarchimedean analysis

• Yaël Dillies (@YaelDillies) t-algebra t-analysis t-combinatorics t-computability t-convex-geometry t-measure-probability t-order t-set-theory

  I am competent for all of combinatorics, all of (algebraic) order theory, all of basic algebra (in particular pointwise actions), most of probability/measure theory, most of convex analysis. For non-mathematical subjects, I have strong opinions on naming and can give advice on type hierarchies and positivity extensions.

• Yury G. Kudryashov (@urkud) t-dynamics t-analysis t-topology t-measure-probability