Basic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

25 declarations, 0 contain sorry, 0 declared as axioms

Problem Formalisation Attributes

The Category Attribute:

Overview

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

A mathematical problem (textbook/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 textbook] : a textbook level math problem.
@[category research open] : an open research level math problem.
@[category research solved] : a solved research 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

The Formal Proof Attribute:

Overview

Provides information about the existence of a formal proof for a statement. This is independent of the category attribute and can be used with any category.

Values

@[formal_proof using formal_conjectures at "link"] : formally proved in this repository.
@[formal_proof using lean4 at "link"] : formally proved in Lean 4 elsewhere.
@[formal_proof using other_system at "link"] : formally proved in another system (Roqc, Isabelle, Lean 3, HOL, etc.)

Conditional formal proofs

A formal proof that only establishes the statement under an unproven hypothesis (such as GRH) is marked with the conditional modifier. Each hypothesis is stated as a declaration in the same file (with a sorry proof) and named in the assuming clause:

@[conditional formal_proof using lean4 at "link" assuming grh] : formally proved in Lean 4 elsewhere, assuming the statement of the declaration grh.

This is the structured counterpart to the conditional_* naming convention already used in the repository (e.g. conditional_artin_primitive_roots): a proof can be sorry-free and still establish the statement only under an unproven hypothesis, so a reader and the site can see exactly what is assumed rather than infer it from a declaration name.

Usage examples

The tag should be used as follows:

@[category textbook]
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 research solved, formal_proof using lean4 at "https://example.com/proof"]
theorem a_solved_problem_with_formal_proof : ... := by
  sorry

/-- The unproven hypothesis assumed by the conditional proof below (statement only). -/
@[category research open]
theorem grh : ... := by
  sorry

@[category research solved,
  conditional formal_proof using lean4 at "https://example.com/proof" assuming grh]
theorem a_conditionally_proved_problem : ... := 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.

Imports (2)

Imported by 7 files

inductive ProblemAttributes.FormalProofKind The type of formal proof that exists for a problem line 138 source

Source documentation

The type of formal proof that exists for a problem.

no axioms what this means

inductive 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). -/
  | formalConjecturesProof
  /-- The problem is solved in Lean 4 (e.g. in Mathlib or some other
  repository), perhaps as an equivalent statement. -/
  | lean4
  /-- The problem is formally solved in a different system (Roqc, Isabelle, Lean 3, HOL, etc.). -/
  | otherSystem
  deriving Inhabited, BEq, Hashable, ToExpr

inductive ProblemAttributes.ProblemStatus line 151 source
no axioms what this means
def ProblemAttributes.formalProofKind.toName line 161 source
no axioms what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr2, List.nil, Option, Lean.Name
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Option.some, Lean.Name.mkStr3, Option.none
2 instances, coercions and auxiliary constants left out.
def ProblemAttributes.problemStatus.toName Convert from a syntax node to a name line 171 source
Source documentation
Convert from a syntax node to a name.

no axioms what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr2, List.nil, Option, Lean.Name
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Option.some, Lean.Name.mkStr3, Option.none
2 instances, coercions and auxiliary constants left out.
```
def problemStatus.toName (stx : TSyntax ``problemStatus) : Option Name :=
…
```

inductive ProblemAttributes.Category A type to capture the various types of statements that appear in our Lean files line 178 source

Source documentation

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

no axioms what this means

inductive Category
  /-- A textbook level math problem (high school, undergraduate, or graduate). -/
  | textbook
  /-- A research level math problem. This can be open, or already solved -/
  | research : ProblemStatus → Category
  /-- A test statement that serves as a sanity check (e.g. for a new definition)-/
  | test
  /-- An "API" statement, i.e. a statement that constructs basic theory around a new definition -/
  | API
  deriving Inhabited, BEq, Hashable, ToExpr

syntax CategorySyntax := &"textbook"
…

Mentions: ProblemAttributes.ProblemStatus, test

structure ProblemAttributes.CategoryTag TODO(lezeau): do we eventually want to account for the problem's source? line 193 source
Source comment
TODO(lezeau): do we eventually want to account for the problem's source?

no axioms what this means
```
structure CategoryTag where
…
```
def ProblemAttributes.addCategoryEntry line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.MonadEnv, Lean.Name, ProblemAttributes.Category, String, Unit
Proof uses: Lean.MonadEnv.modifyEnv, Lean.Environment, Lean.PersistentEnvExtension.addEntry, ProblemAttributes.CategoryTag, Prod, List, Std.HashSet, ProblemAttributes.categoryExt, ProblemAttributes.CategoryTag.mk, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.
structure ProblemAttributes.FormalProofTag A tag recording the existence and location of a formal proof for a declaration line 216 source
Source documentation
A tag recording the existence and location of a formal proof for a declaration.

no axioms what this means
```
structure FormalProofTag where
…
```
def ProblemAttributes.addFormalProofEntry line 236 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.MonadEnv, Lean.Name, ProblemAttributes.FormalProofKind, String, optParam, List, List.nil, Unit
Proof uses: Lean.MonadEnv.modifyEnv, Lean.Environment, Lean.PersistentEnvExtension.addEntry, ProblemAttributes.FormalProofTag, Prod, Std.HashSet, ProblemAttributes.formalProofExt, ProblemAttributes.FormalProofTag.mk, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.
structure ProblemAttributes.SubjectTag line 243 source
no axioms what this means
def ProblemAttributes.addSubjectEntry line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.MonadEnv, Lean.Name, List, AMS, String, Unit
Proof uses: Lean.MonadEnv.modifyEnv, Lean.Environment, Lean.PersistentEnvExtension.addEntry, ProblemAttributes.SubjectTag, Prod, Std.HashSet, ProblemAttributes.subjectExt, ProblemAttributes.SubjectTag.mk, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.
def ProblemAttributes.Syntax.toCategory Convert from a syntax node to a term of type Category and annotate the syntax with the corresponding name's docstring line 267 source
Source documentation
Convert from a syntax node to a term of type Category and annotate the syntax with the corresponding name's docstring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr2, List.nil, Lean.Core.CoreM, ProblemAttributes.Category
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Bind.bind, Unit, Lean.Elab.addConstInfo, Lean.Name.mkStr3, Option.none, Lean.Expr, Pure.pure, Lean.Core.Context, StateRefT', IO.RealWorld and 58 more
38 instances, coercions and auxiliary constants left out.
```
def Syntax.toCategory (stx : TSyntax ``CategorySyntax) : CoreM Category := do
…
```
Mentions: ProblemAttributes.Category
def ProblemAttributes.toCategorySyntax Extract the category attributes from a declaration's modifiers line 294 source
Source documentation
Extract the category attributes from a declaration's modifiers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr4, List.nil, Lean.Elab.Command.CommandElabM, Array
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Lean.Syntax.matchesNull, Option, Array.mapM, Lean.TSyntax.mk, Option.some, Array.getSepElems, Lean.Syntax.getArgs, Array.filterM, Lean.Name.mkStr2, Pure.pure and 10 more
9 instances, coercions and auxiliary constants left out.
```
def toCategorySyntax
    (stx : TSyntax ``Command.declModifiers) :
    CommandElabM (Array <| TSyntax ``attrInstance) := do
…
```
def ProblemAttributes.toCategories Extract the categories from a declaration's modifiers line 306 source
Source documentation
Extract the categories from a declaration's modifiers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr4, List.nil, Lean.Elab.Command.CommandElabM, Array, ProblemAttributes.Category
Proof uses: Bind.bind, ProblemAttributes.toCategorySyntax, Array.mapM, Lean.Syntax, ite, Eq, Bool, Lean.Syntax.isOfKind, Bool.true, Lean.Syntax.getArg, OfNat.ofNat, Nat, Lean.Syntax.matchesNull, Lean.Name.mkStr2, Lean.TSyntax.mk, Lean.Elab.Command.liftCoreM, ProblemAttributes.Syntax.toCategory, Lean.Elab.throwUnsupportedSyntax, Lean.TSyntaxArray.raw
5 instances, coercions and auxiliary constants left out.
```
def toCategories
    (stx : TSyntax ``Command.declModifiers) :
    CommandElabM (Array Category) := do
…
```
Mentions: ProblemAttributes.Category
def ProblemAttributes.addFormalProofAttribute Records the existence and location of a formal proof for a statement line 368 source
Source documentation
Records the existence and location of a formal proof for a statement.
Usage: @[formal_proof using <kind> at "<link>"] where <kind> is one of:
- formal_conjectures : formally proved in this repository.
- lean4 : formally proved in Lean 4 elsewhere (e.g. Mathlib).
- other_system : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.)
This says a proof of this statement exists somewhere, so in practice it goes on problems we already consider settled, and attaching it to a research open problem warns. To record a conditional result about a problem that is still open, state the implication as its own research solved variant carrying the assumption as a hypothesis, and annotate that.
conditional is for something else: the proof at the link establishes the statement only under hypotheses the author has not proved. That is a fact about their proof, not about the problem's status, and it is not visible from the proof term. #print axioms on a proof that takes its assumption as a parameter comes back clean, so it has to be written down:
@[conditional formal_proof using <kind> at "<link>" assuming <decl> ...]
Each named hypothesis is a declaration in the same file, stated with a sorry proof, so a reader can see what is being assumed.
L4DEL explanation
Records the existence and location of a formal proof for a statement. Usage: @[formal_proof using at ""] where `` is one of: - formal_conjectures : formally proved in this repository. - lean4 : formally proved in Lean 4 elsewhere (e.g. Mathlib). - other_system : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.) This says a proof of this statement exists somewhere, so in practice it goes on problems we already consider settled, and attaching it to a research open problem warns. To record a conditional result about a problem that is still open, state the implication as its own research solved variant carrying the assumption as a hypothesis, and annotate that. conditional is for something else: the proof at the link establishes the statement only under hypotheses the author has not proved. That is a fact about their proof, not about the problem's status, and it is not visible from the proof term. #print axioms on a proof that takes its assumption as a parameter comes back clean, so it has to be written down: @[conditional formal_proof using at "" assuming ...] Each named hypothesis is a declaration in the same file, stated with a sorry proof, so a reader can see what is being assumed.
Sources and attribution: Pinned Lean source (1646ca16afd6)
```
private def addFormalProofAttribute (decl : Name) (stx : Syntax) : AttrM Unit := do
…
```
def ProblemAttributes.Syntax.toSubjects Converts a syntax node to an array of AMS subjects line 435 source
Source documentation
Converts a syntax node to an array of AMS subjects.
This also annotates every natural number literal encountered with the description of the corresponding AMS subject (i.e. hovering over the number in VS Code will show the subject.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr2, List.nil, Lean.Meta.MetaM, Array, AMS
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Option, Lean.Name.mkStr1, Array.mapM, Lean.TSyntax.mk, Option.some, Lean.Syntax.getArgs, Lean.TSyntax.getNat, Bind.bind, Lean.Name, numToAMSName and 11 more
23 instances, coercions and auxiliary constants left out.
```
def Syntax.toSubjects (stx : TSyntax ``subjectList) : MetaM (Array AMS) := do
…
```
Mentions: AMS
def ProblemAttributes.splitByFun Split an array into preimages of a function line 471 source
Source documentation
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

standard axioms: Quot.sound, propext what this means
Statement uses: BEq, Hashable, Array, Std.HashMap
Proof uses: Array.foldr, EmptyCollection.emptyCollection, Array.size, OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.
```
def splitByFun {α β : Type} (f : α → β) [BEq β] [Hashable β]
    (arr : Array α) : Std.HashMap β (Array α) :=
…
```
def ProblemAttributes.getTags line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Array, ProblemAttributes.CategoryTag
Proof uses: Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, Pure.pure, Std.HashSet.toArray, Lean.SimplePersistentEnvExtension.getState, Std.HashSet, ProblemAttributes.categoryExt, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Prod, List, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.
def ProblemAttributes.getStatementTags line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Std.HashMap, ProblemAttributes.Category, Array, ProblemAttributes.CategoryTag
Proof uses: Bind.bind, ProblemAttributes.getTags, Pure.pure, ProblemAttributes.splitByFun, ProblemAttributes.CategoryTag.category
7 instances, coercions and auxiliary constants left out.
def ProblemAttributes.getCategoryStats line 490 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, ProblemAttributes.Category, Nat
Proof uses: Bind.bind, Std.HashMap, Array, ProblemAttributes.CategoryTag, ProblemAttributes.getStatementTags, Pure.pure, Std.HashMap.getD, Std.HashMap.map, Array.size, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
def ProblemAttributes.getSubjectTags line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Array, ProblemAttributes.SubjectTag
Proof uses: Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, Pure.pure, Std.HashSet.toArray, Lean.SimplePersistentEnvExtension.getState, Std.HashSet, ProblemAttributes.subjectExt, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Prod, List, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.
def ProblemAttributes.getFormalProofTags line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Array, ProblemAttributes.FormalProofTag
Proof uses: Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, Pure.pure, Std.HashSet.toArray, Lean.SimplePersistentEnvExtension.getState, Std.HashSet, ProblemAttributes.formalProofExt, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Prod, List, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.
def ProblemAttributes.getFormalProofTag Get the formal proof tag for a given declaration, if any line 501 source
Source documentation
Get the formal proof tag for a given declaration, if any.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Lean.Name, Option, ProblemAttributes.FormalProofTag
Proof uses: Bind.bind, Array, ProblemAttributes.getFormalProofTags, Pure.pure, Array.find?, BEq.beq, ProblemAttributes.FormalProofTag.declName
4 instances, coercions and auxiliary constants left out.
```
def getFormalProofTag (declName : Name) : m (Option FormalProofTag) := do
…
```
Mentions: ProblemAttributes.FormalProofTag
def ProblemAttributes.getProofConditions Get the unproven hypotheses a given declaration's formal proof assumes line 507 source
Source documentation
Get the unproven hypotheses a given declaration's formal proof assumes. Empty when there is no formal proof or the proof is unconditional.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadEnv, Lean.Name, List
Proof uses: Bind.bind, Option, ProblemAttributes.FormalProofTag, ProblemAttributes.getFormalProofTag, Pure.pure, Option.getD, Option.map, ProblemAttributes.FormalProofTag.conditions, List.nil
3 instances, coercions and auxiliary constants left out.
```
def getProofConditions (declName : Name) : m (List Name) := do
…
```
def ProblemAttributes.verifyCategoryCounts Verify that the list of problems contains the expected number of problems for each category line 515 source
Source documentation
Verify that the list of problems contains the expected number of problems for each category. Throws an error if counts do not match.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Lean.Name, Prod, String, Nat, Lean.Meta.MetaM, Unit
Proof uses: Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, Std.HashSet, ProblemAttributes.CategoryTag, Lean.SimplePersistentEnvExtension.getState, ProblemAttributes.categoryExt, Lean.EnvExtension.asyncMode, Lean.PersistentEnvExtensionState, Lean.PersistentEnvExtension.toEnvExtension, Lean.Name.anonymous, List.nil, Option, List.find?, BEq.beq, Prod.fst, List.cons, Prod.mk, HAdd.hAdd, OfNat.ofNat and 39 more
43 instances, coercions and auxiliary constants left out.
```
def verifyCategoryCounts (problems : List Name) (expected : List (String × Nat)) : MetaM Unit := do
…
```