AMS Subject classification

This file defines some tools used by the ProblemSubject attribute in order classify problems by their corresponding AMS Subject.

The AMSDescription has one term for each number n ∈ {1, ..., 96} that has a corresponding AMS subject, namely AMSDescription.«n». Note that not all values of n in this interval are assigned a subject.

To extract the value corresponding to n, one can use numToAMSDescriptions n. This is useful for getting the doctring that corresponds to the subject n when parsing the attribute.

Finally, to access the list of subjects and their corresponding number when editing Lean files, we implement a #AMS command that prints this list.

inductive AMS : Type

• «0» : AMS

  General and overarching topics

• «1» : AMS

  History and biography

• «3» : AMS

  Mathematical logic and foundations

• «5» : AMS

  Combinatorics

• «6» : AMS

  Order, lattices, ordered algebraic structures

• «8» : AMS

  General algebraic systems

• «11» : AMS

  Number theory

• «12» : AMS

  Field theory and polynomials

• «13» : AMS

  Commutative algebra

• «14» : AMS

  Algebraic geometry

• «15» : AMS

  Linear and multilinear algebra; matrix theory

• «16» : AMS

  Associative rings and algebras

• «17» : AMS

  Nonassociative rings and algebras

• «18» : AMS

  Category theory; homological algebra

• «19» : AMS

  K-theory

• «20» : AMS

  Group theory and generalizations

• «22» : AMS

  Topological groups, Lie groups

• «26» : AMS

  Real functions

• «28» : AMS

  Measure and integration

• «30» : AMS

  Functions of a complex variable

• «31» : AMS

  Potential theory

• «32» : AMS

  Several complex variables and analytic spaces

• «33» : AMS

  Special functions

• «34» : AMS

  Ordinary differential equations

• «35» : AMS

  Partial differential equations

• «37» : AMS

  Dynamical systems and ergodic theory

• «39» : AMS

  Difference and functional equations

• «40» : AMS

  Sequences, series, summability

• «41» : AMS

  Approximations and expansions

• «42» : AMS

  Harmonic analysis on Euclidean spaces

• «43» : AMS

  Abstract harmonic analysis

• «44» : AMS

  Integral transforms, operational calculus

• «45» : AMS

  Integral equations

• «46» : AMS

  Functional analysis

• «47» : AMS

  Operator theory

• «49» : AMS

  Calculus of variations and optimal control; optimization

• «51» : AMS

  Geometry

• «52» : AMS

  Convex and discrete geometry

• «53» : AMS

  Differential geometry

• «54» : AMS

  General topology

• «55» : AMS

  Algebraic topology

• «57» : AMS

  Manifolds and cell complexes

• «58» : AMS

  Global analysis, analysis on manifolds

• «60» : AMS

  Probability theory and stochastic processes

• «62» : AMS

  Statistics

• «65» : AMS

  Numerical analysis

• «68» : AMS

  Computer science

• «70» : AMS

  Mechanics of particles and systems

• «74» : AMS

  Mechanics of deformable solids

• «76» : AMS

  Fluid mechanics

• «78» : AMS

  Optics, electromagnetic theory

• «80» : AMS

  Classical thermodynamics, heat transfer

• «81» : AMS

  Quantum theory

• «82» : AMS

  Statistical mechanics, structure of matter

• «83» : AMS

  Relativity and gravitational theory

• «85» : AMS

  Astronomy and astrophysics

• «86» : AMS

  Geophysics

• «90» : AMS

  Operations research, mathematical programming

• «91» : AMS

  Game theory, economics, social and behavioral sciences

• «92» : AMS

  Biology and other natural sciences

• «93» : AMS

  Systems theory; control

• «94» : AMS

  Information and communication, circuits

• «97» : AMS

  Mathematics education

instance instInhabitedAMS : Inhabited AMS

Equations

• instInhabitedAMS = { default := AMS.«0» }

instance instBEqAMS : BEq AMS

Equations

• instBEqAMS = { beq := beqAMS✝ }

instance instHashableAMS : Hashable AMS

Equations

• instHashableAMS = { hash := hashAMS✝ }

instance instToExprAMS : Lean.ToExpr AMS

Equations

• instToExprAMS = { toExpr := toExprAMS✝, toTypeExpr := Lean.Expr.const `AMS [] }

def numToAMSName (n : Nat) : Lean.MetaM Lean.Name

Equations

• One or more equations did not get rendered due to their size.

def AMS.getDesc (a : AMS) : Lean.CoreM String

Equations

• One or more equations did not get rendered due to their size.

def AMS.toNat? (a : AMS) : Option Nat

Equations

• a.toNat? = match Lean.toExpr a with | Lean.Expr.const (pre.str m) [] => m.toNat? | x => none

unsafe def numToAMSSubjects (n : Nat) : Lean.MetaM AMS

Equations

• numToAMSSubjects n = do let nm ← numToAMSName n Lean.Meta.evalExpr AMS q(AMS) (Lean.Expr.const nm [])

def «command#AMS» : Lean.ParserDescr

The #AMS outputs a list of the AMS Math Subjects and their correponding indices

Equations

• «command#AMS» = Lean.ParserDescr.node `«command#AMS» 1024 (Lean.ParserDescr.symbol "#AMS")