Documentation

FormalConjectures.Util.Attributes.Basic

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 research formally solved using <kind> at "link"]: a formally solved research problem. `<kind>` must be one of:
- formal_conjectures : solved in this repository (e.g. filling the sorry in the current file).
- lean4 : solved in Lean 4 (e.g. Mathlib, or some other repo) as an equivalent statement.
- other_system : solved in another formal system (Roqc, Isabelle, Lean3, HOL, etc.).
@[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.FormalProofKind :

The type of formal proof that exists for a problem. This is meant to be used for the research formally solved category.

formalConjecturesProof : FormalProofKind
The problem exactly as stated in formal-conjectures has a formal proof. The link points to a commit that fills the sorry relative to the current commit (i.e., the commit where this category is added, or the commit with the latest fix for this statement).
lean4 : FormalProofKind
The problem is solved in Lean 4 (e.g. in Mathlib or some other repository), perhaps as an equivalent statement.
otherSystem : FormalProofKind
The problem is formally solved in a different system (Roqc, Isabelle, Lean 3, HOL, etc.).

Instances For

def ProblemAttributes.instInhabitedFormalProofKind.default :

FormalProofKind

Equations

ProblemAttributes.instInhabitedFormalProofKind.default = ProblemAttributes.FormalProofKind.formalConjecturesProof

Instances For

instance ProblemAttributes.instInhabitedFormalProofKind :

Inhabited FormalProofKind

Equations

ProblemAttributes.instInhabitedFormalProofKind = { default := ProblemAttributes.instInhabitedFormalProofKind.default }

instance ProblemAttributes.instBEqFormalProofKind :

BEq FormalProofKind

Equations

ProblemAttributes.instBEqFormalProofKind = { beq := ProblemAttributes.instBEqFormalProofKind.beq }

def ProblemAttributes.instBEqFormalProofKind.beq :

FormalProofKind → FormalProofKind → Bool

Equations

ProblemAttributes.instBEqFormalProofKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance ProblemAttributes.instHashableFormalProofKind :

Hashable FormalProofKind

Equations

ProblemAttributes.instHashableFormalProofKind = { hash := ProblemAttributes.instHashableFormalProofKind.hash }

def ProblemAttributes.instHashableFormalProofKind.hash :

FormalProofKind → UInt64

Equations

Instances For

def ProblemAttributes.instToExprFormalProofKind.toExpr :

FormalProofKind → Lean.Expr

Equations

ProblemAttributes.instToExprFormalProofKind.toExpr ProblemAttributes.FormalProofKind.formalConjecturesProof = Lean.Expr.const `ProblemAttributes.FormalProofKind.formalConjecturesProof []
ProblemAttributes.instToExprFormalProofKind.toExpr ProblemAttributes.FormalProofKind.lean4 = Lean.Expr.const `ProblemAttributes.FormalProofKind.lean4 []
ProblemAttributes.instToExprFormalProofKind.toExpr ProblemAttributes.FormalProofKind.otherSystem = Lean.Expr.const `ProblemAttributes.FormalProofKind.otherSystem []

Instances For

instance ProblemAttributes.instToExprFormalProofKind :

Lean.ToExpr FormalProofKind

Equations

ProblemAttributes.instToExprFormalProofKind = { toExpr := ProblemAttributes.instToExprFormalProofKind.toExpr, toTypeExpr := Lean.Expr.const `ProblemAttributes.FormalProofKind [] }

inductive ProblemAttributes.ProblemStatus :

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.
formallySolvedAt : FormalProofKind → String → ProblemStatus
Indicates that a mathematical problem is formally solved in this repository, with a link to the formal proof.

Instances For

instance ProblemAttributes.instInhabitedProblemStatus :

Inhabited ProblemStatus

Equations

ProblemAttributes.instInhabitedProblemStatus = { default := ProblemAttributes.instInhabitedProblemStatus.default }

def ProblemAttributes.instInhabitedProblemStatus.default :

Equations

ProblemAttributes.instInhabitedProblemStatus.default = ProblemAttributes.ProblemStatus.open

Instances For

instance ProblemAttributes.instBEqProblemStatus :

BEq ProblemStatus

Equations

ProblemAttributes.instBEqProblemStatus = { beq := ProblemAttributes.instBEqProblemStatus.beq }

def ProblemAttributes.instHashableProblemStatus.hash :

ProblemStatus → UInt64

Equations

Instances For

instance ProblemAttributes.instHashableProblemStatus :

Hashable ProblemStatus

Equations

ProblemAttributes.instHashableProblemStatus = { hash := ProblemAttributes.instHashableProblemStatus.hash }

def ProblemAttributes.instToExprProblemStatus.toExpr :

ProblemStatus → Lean.Expr

Equations

One or more equations did not get rendered due to their size.
ProblemAttributes.instToExprProblemStatus.toExpr ProblemAttributes.ProblemStatus.open = Lean.Expr.const `ProblemAttributes.ProblemStatus.open []
ProblemAttributes.instToExprProblemStatus.toExpr ProblemAttributes.ProblemStatus.solved = Lean.Expr.const `ProblemAttributes.ProblemStatus.solved []

Instances For

instance ProblemAttributes.instToExprProblemStatus :

Lean.ToExpr ProblemStatus

Equations

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

def ProblemAttributes.formalProofKind :

Lean.ParserDescr

Equations

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

Instances For

def ProblemAttributes.formalProofKind.toName (stx : Lean.TSyntax `ProblemAttributes.formalProofKind) :

Option Lean.Name

Equations

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

Instances For

def ProblemAttributes.problemStatus :

Lean.ParserDescr

Equations

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

Instances For

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.

Instances For

inductive ProblemAttributes.Category :

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

Instances For

instance ProblemAttributes.instInhabitedCategory :

Inhabited Category

Equations

ProblemAttributes.instInhabitedCategory = { default := ProblemAttributes.instInhabitedCategory.default }

def ProblemAttributes.instInhabitedCategory.default :

Equations

ProblemAttributes.instInhabitedCategory.default = ProblemAttributes.Category.highSchool

Instances For

def ProblemAttributes.instBEqCategory.beq :

Category → Category → Bool

Equations

Instances For

instance ProblemAttributes.instBEqCategory :

Equations

ProblemAttributes.instBEqCategory = { beq := ProblemAttributes.instBEqCategory.beq }

instance ProblemAttributes.instHashableCategory :

Hashable Category

Equations

ProblemAttributes.instHashableCategory = { hash := ProblemAttributes.instHashableCategory.hash }

instance ProblemAttributes.instToExprCategory :

Lean.ToExpr Category

Equations

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

def ProblemAttributes.instToExprCategory.toExpr :

Category → Lean.Expr

Equations

ProblemAttributes.instToExprCategory.toExpr ProblemAttributes.Category.highSchool = Lean.Expr.const `ProblemAttributes.Category.highSchool []
ProblemAttributes.instToExprCategory.toExpr ProblemAttributes.Category.undergraduate = Lean.Expr.const `ProblemAttributes.Category.undergraduate []
ProblemAttributes.instToExprCategory.toExpr ProblemAttributes.Category.graduate = Lean.Expr.const `ProblemAttributes.Category.graduate []
ProblemAttributes.instToExprCategory.toExpr (ProblemAttributes.Category.research a) = (Lean.Expr.const `ProblemAttributes.Category.research []).app (Lean.toExpr a)
ProblemAttributes.instToExprCategory.toExpr ProblemAttributes.Category.test = Lean.Expr.const `ProblemAttributes.Category.test []
ProblemAttributes.instToExprCategory.toExpr ProblemAttributes.Category.API = Lean.Expr.const `ProblemAttributes.Category.API []

Instances For

def ProblemAttributes.CategorySyntax :

Lean.ParserDescr

Equations

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

Instances For

structure ProblemAttributes.CategoryTag :

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.

Instances For

instance ProblemAttributes.instInhabitedCategoryTag :

Inhabited CategoryTag

Equations

ProblemAttributes.instInhabitedCategoryTag = { default := ProblemAttributes.instInhabitedCategoryTag.default }

def ProblemAttributes.instInhabitedCategoryTag.default :

Equations

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

Instances For

instance ProblemAttributes.instBEqCategoryTag :

BEq CategoryTag

Equations

ProblemAttributes.instBEqCategoryTag = { beq := ProblemAttributes.instBEqCategoryTag.beq }

def ProblemAttributes.instBEqCategoryTag.beq :

CategoryTag → CategoryTag → Bool

Equations

ProblemAttributes.instBEqCategoryTag.beq { declName := a, category := a_1, informal := a_2 } { declName := b, category := b_1, informal := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
ProblemAttributes.instBEqCategoryTag.beq x✝¹ x✝ = false

Instances For

instance ProblemAttributes.instHashableCategoryTag :

Hashable CategoryTag

Equations

ProblemAttributes.instHashableCategoryTag = { hash := ProblemAttributes.instHashableCategoryTag.hash }

def ProblemAttributes.instHashableCategoryTag.hash :

CategoryTag → UInt64

Equations

ProblemAttributes.instHashableCategoryTag.hash { declName := a, category := a_1, informal := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

Instances For

instance ProblemAttributes.instToExprCategoryTag :

Lean.ToExpr CategoryTag

Equations

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

def ProblemAttributes.instToExprCategoryTag.toExpr :

CategoryTag → Lean.Expr

Equations

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

Instances For

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) :

Equations

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

Instances For

structure ProblemAttributes.SubjectTag :

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.

Instances For

def ProblemAttributes.instInhabitedSubjectTag.default :

Equations

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

Instances For

instance ProblemAttributes.instInhabitedSubjectTag :

Inhabited SubjectTag

Equations

ProblemAttributes.instInhabitedSubjectTag = { default := ProblemAttributes.instInhabitedSubjectTag.default }

instance ProblemAttributes.instBEqSubjectTag :

Equations

ProblemAttributes.instBEqSubjectTag = { beq := ProblemAttributes.instBEqSubjectTag.beq }

def ProblemAttributes.instBEqSubjectTag.beq :

SubjectTag → SubjectTag → Bool

Equations

ProblemAttributes.instBEqSubjectTag.beq { declName := a, subjects := a_1, informal := a_2 } { declName := b, subjects := b_1, informal := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
ProblemAttributes.instBEqSubjectTag.beq x✝¹ x✝ = false

Instances For

def ProblemAttributes.instHashableSubjectTag.hash :

SubjectTag → UInt64

Equations

ProblemAttributes.instHashableSubjectTag.hash { declName := a, subjects := a_1, informal := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

Instances For

instance ProblemAttributes.instHashableSubjectTag :

Hashable SubjectTag

Equations

ProblemAttributes.instHashableSubjectTag = { hash := ProblemAttributes.instHashableSubjectTag.hash }

def ProblemAttributes.instToExprSubjectTag.toExpr :

SubjectTag → Lean.Expr

Equations

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

Instances For

instance ProblemAttributes.instToExprSubjectTag :

Lean.ToExpr SubjectTag

Equations

ProblemAttributes.instToExprSubjectTag = { toExpr := ProblemAttributes.instToExprSubjectTag.toExpr, 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) :

Equations

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

Instances For

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.

Instances For

def ProblemAttributes.Category_attr :

Lean.ParserDescr

Equations

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

Instances For

def ProblemAttributes.subjectList :

Lean.ParserDescr

Equations

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

Instances For

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.

Instances For

def ProblemAttributes.problemSubject :

Lean.ParserDescr

Equations

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

Instances For

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

Instances For

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)

Instances For

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]

Instances For

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

Instances For

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)

Instances For

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.

Instances For

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

Instances For