Problem Formalisation Attributes

The Category Attribute:

Overview

Provides information of the type of a statement. This can be:

• A mathematical problem (high school/undergraduate/graduate/research level). If this is a research problem then the user is also required to specify whether the problem has already been solved.
• An API statement
• A "test" statement

Values

The values of this attribute are

• @[category high_school] : a high school level math problem.
• @[category undergraduate] : an undergraduate level math problem.
• @[category graduate] : a graduate level math problem.
• @[category research open] : an open reseach level math problem.
• @[category research solved] : a solved reseach level math problem. The criterion for being solved is that there exists an informal solution that is widely accepted by experts in the area. In particular, this does not require a formal solution to exist.
• @[category test] : a statement that serves as a sanity check (e.g. for a new definition).
• @[category API] : a statement that constructs basic theory around a new definition

Usage examples

The tag should be used as follows:

@[category high_school]
theorem imo_2024_p6
    (IsAquaesulian : (ℚ → ℚ) → Prop)
    (IsAquaesulian_def : ∀ f, IsAquaesulian f ↔
      ∀ x y, f (x + f y) = f x + y ∨ f (f x + y) = x + f y) :
    IsLeast {(c : ℤ) | ∀ f, IsAquaesulian f → {(f r + f (-r)) | (r : ℚ)}.Finite ∧
      {(f r + f (-r)) | (r : ℚ)}.ncard ≤ c} 2 := by
  sorry

@[category research open]
theorem an_open_problem : Transcendental ℝ (π + rexp 1) := by
  sorry

@[category test]
theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := by
  sorry

The Problem Subject Attribute

Provides information about the subject of a mathematical problem, via a numeral corresponding to the AMS subject classification of the problem. This can be used as follows:

@[AMS 11] -- 11 correponds to Number Theory in the AMS classification
theorem FLT : FermatLastTheorem := by
  sorry

The complete list of subjects can be found here: https://mathscinet.ams.org/mathscinet/msc/pdfs/classifications2020.pdf

In order to access the list from within a Lean file, use the #AMS command.

Note: the current implementation of the attribute includes all the main categories in the AMS classification for completeness. Some are not relevant to this repository.

inductive ProblemAttributes.ProblemStatus : Type

• open : ProblemStatus

  Indicates that a mathematical problem is still open.

• solved : ProblemStatus

  Indicates that a mathematical problem is already solved, i.e., there is a published (informal) proof that is widely accepted by experts.

instance ProblemAttributes.instInhabitedProblemStatus : Inhabited ProblemStatus

Equations

• ProblemAttributes.instInhabitedProblemStatus = { default := ProblemAttributes.ProblemStatus.open }

instance ProblemAttributes.instBEqProblemStatus : BEq ProblemStatus

Equations

• ProblemAttributes.instBEqProblemStatus = { beq := ProblemAttributes.beqProblemStatus✝ }

instance ProblemAttributes.instHashableProblemStatus : Hashable ProblemStatus

Equations

• ProblemAttributes.instHashableProblemStatus = { hash := ProblemAttributes.hashProblemStatus✝ }

instance ProblemAttributes.instToExprProblemStatus : Lean.ToExpr ProblemStatus

Equations

• ProblemAttributes.instToExprProblemStatus = { toExpr := ProblemAttributes.toExprProblemStatus✝, toTypeExpr := Lean.Expr.const `ProblemAttributes.ProblemStatus [] }

def ProblemAttributes.problemStatus : Lean.ParserDescr

Equations

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

def ProblemAttributes.problemStatus.toName (stx : Lean.TSyntax `ProblemAttributes.problemStatus) : Option Lean.Name

Convert from a syntax node to a name.

Equations

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

inductive ProblemAttributes.Category : Type

A type to capture the various types of statements that appear in our Lean files.

• highSchool : Category

  A high school level math problem.

• undergraduate : Category

  An undegraduate level math problem.

• graduate : Category

  A graduate level math problem.

• research : ProblemStatus → Category

  A reseach level math problem. This can be open, or already solved

• test : Category

  A test statement that serves as a sanity check (e.g. for a new definition)

• API : Category

  An "API" statement, i.e. a statement that constructs basic theory around a new definition

instance ProblemAttributes.instInhabitedCategory : Inhabited Category

Equations

• ProblemAttributes.instInhabitedCategory = { default := ProblemAttributes.Category.highSchool }

instance ProblemAttributes.instBEqCategory : BEq Category

Equations

• ProblemAttributes.instBEqCategory = { beq := ProblemAttributes.beqCategory✝ }

instance ProblemAttributes.instHashableCategory : Hashable Category

Equations

• ProblemAttributes.instHashableCategory = { hash := ProblemAttributes.hashCategory✝ }

instance ProblemAttributes.instToExprCategory : Lean.ToExpr Category

Equations

• ProblemAttributes.instToExprCategory = { toExpr := ProblemAttributes.toExprCategory✝, toTypeExpr := Lean.Expr.const `ProblemAttributes.Category [] }

def ProblemAttributes.CategorySyntax : Lean.ParserDescr

Equations

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

structure ProblemAttributes.CategoryTag : Type

• declName : Lean.Name

  The name of the declaration with the given tag.

• category : Category

  The status of the problem.

• informal : String

  The (optional) comment that comes with the given declaration.

instance ProblemAttributes.instInhabitedCategoryTag : Inhabited CategoryTag

Equations

• ProblemAttributes.instInhabitedCategoryTag = { default := { declName := default, category := default, informal := default } }

instance ProblemAttributes.instBEqCategoryTag : BEq CategoryTag

Equations

• ProblemAttributes.instBEqCategoryTag = { beq := ProblemAttributes.beqCategoryTag✝ }

instance ProblemAttributes.instHashableCategoryTag : Hashable CategoryTag

Equations

• ProblemAttributes.instHashableCategoryTag = { hash := ProblemAttributes.hashCategoryTag✝ }

instance ProblemAttributes.instToExprCategoryTag : Lean.ToExpr CategoryTag

Equations

• ProblemAttributes.instToExprCategoryTag = { toExpr := ProblemAttributes.toExprCategoryTag✝, toTypeExpr := Lean.Expr.const `ProblemAttributes.CategoryTag [] }

opaque ProblemAttributes.categoryExt : Lean.SimplePersistentEnvExtension CategoryTag (Std.HashSet CategoryTag)

Defines the categoryExt extension for adding a HashSet of Tags to the environment.

def ProblemAttributes.addCategoryEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) (cat : Category) (comment : String) : m Unit

Equations

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

structure ProblemAttributes.SubjectTag : Type

• declName : Lean.Name

  The name of the declaration with the given tag.

• subjects : List AMS

  The subject(s) of the problem.

• informal : String

  The (optional) comment that comes with the given declaration.

instance ProblemAttributes.instInhabitedSubjectTag : Inhabited SubjectTag

Equations

• ProblemAttributes.instInhabitedSubjectTag = { default := { declName := default, subjects := default, informal := default } }

instance ProblemAttributes.instBEqSubjectTag : BEq SubjectTag

Equations

• ProblemAttributes.instBEqSubjectTag = { beq := ProblemAttributes.beqSubjectTag✝ }

instance ProblemAttributes.instHashableSubjectTag : Hashable SubjectTag

Equations

• ProblemAttributes.instHashableSubjectTag = { hash := ProblemAttributes.hashSubjectTag✝ }

instance ProblemAttributes.instToExprSubjectTag : Lean.ToExpr SubjectTag

Equations

• ProblemAttributes.instToExprSubjectTag = { toExpr := ProblemAttributes.toExprSubjectTag✝, toTypeExpr := Lean.Expr.const `ProblemAttributes.SubjectTag [] }

opaque ProblemAttributes.subjectExt : Lean.SimplePersistentEnvExtension SubjectTag (Std.HashSet SubjectTag)

Defines the tagExt extension for adding a HashSet of Tags to the environment.

def ProblemAttributes.addSubjectEntry {m : Type → Type} [Lean.MonadEnv m] (name : Lean.Name) (subjects : List AMS) (informal : String) : m Unit

Equations

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

def ProblemAttributes.Syntax.toCategory (stx : Lean.TSyntax `ProblemAttributes.CategorySyntax) : Lean.CoreM Category

Convert from a syntax node to a term of type Category and annotate the syntax with the corresponding name's docstring.

Equations

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

def ProblemAttributes.Category_attr : Lean.ParserDescr

Equations

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

def ProblemAttributes.subjectList : Lean.ParserDescr

Equations

• ProblemAttributes.subjectList = Lean.ParserDescr.nodeWithAntiquot "subjectList" `ProblemAttributes.subjectList (Lean.ParserDescr.unary `many (Lean.ParserDescr.const `num))

def ProblemAttributes.Syntax.toSubjects (stx : Lean.TSyntax `ProblemAttributes.subjectList) : Lean.MetaM (Array AMS)

Converts a syntax node to an array of AMS subjects.

This also annotates the every natural number litteral encountered, with the description of the corresponding AMS subject (i.e. hovering over the number in VS Code will show the subject.)

Equations

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

def ProblemAttributes.problemSubject : Lean.ParserDescr

Equations

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

def ProblemAttributes.splitByFun {α β : Type} (f : α → β) [BEq β] [Hashable β] (arr : Array α) : Std.HashMap β (Array α)

Split an array into preimages of a function.

splitByFun f arr is the hashmap such that the value for key b : β is the array of a : α in arr that get mapped to b by f

Equations

• ProblemAttributes.splitByFun f arr = Array.foldr (ProblemAttributes.splitByFun.addPreimage f) ∅ arr

def ProblemAttributes.splitByFun.addPreimage {α β : Type} (f : α → β) [BEq β] [Hashable β] (a : α) (m : Std.HashMap β (Array α)) : Std.HashMap β (Array α)

Equations

• ProblemAttributes.splitByFun.addPreimage f a m = m.alter (f a) (ProblemAttributes.splitByFun.appendIfExists a)

def ProblemAttributes.splitByFun.appendIfExists {α : Type} (a : α) : Option (Array α) → Option (Array α)

Equations

• ProblemAttributes.splitByFun.appendIfExists a (some arr) = some (arr.push a)
• ProblemAttributes.splitByFun.appendIfExists a none = some #[a]

def ProblemAttributes.getTags {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Array CategoryTag)

Equations

• ProblemAttributes.getTags = do let __do_lift ← Lean.getEnv pure (ProblemAttributes.categoryExt.getState __do_lift).toArray

def ProblemAttributes.getStatementTags {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Std.HashMap Category (Array CategoryTag))

Equations

• ProblemAttributes.getStatementTags = do let __do_lift ← ProblemAttributes.getTags pure (ProblemAttributes.splitByFun ProblemAttributes.CategoryTag.category __do_lift)

def ProblemAttributes.getCategoryStats {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Category → Nat)

Equations

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

def ProblemAttributes.getSubjectTags {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Array SubjectTag)

Equations

• ProblemAttributes.getSubjectTags = do let __do_lift ← Lean.getEnv pure (ProblemAttributes.subjectExt.getState __do_lift).toArray