RFC: Ideas for New Lean Attributes

[AdamSobieski]

Introduction

Hello. Here are some ideas for new Lean attributes. While Lean 4 supports user attributes, attributes like the ones indicated below, for the following use cases, might be best delivered as built-ins, provided in either core Lean or mathlib.

Use Cases

Search

Creating or using an existing ontology for mathematical metadata would enable enhancing Loogle search capabilities.

Topics for a mathematical metadata ontology include expressing original discovers, transcribers/formalizers, pertinent organizations, dates of discovery and transcription, objects' natural-language titles and descriptions, categories (MSC2020), keywords, and much more.

@[discoverer (value := "Gottfried Wilhelm Leibniz", date := "...")]
@[transcriber (value := "Alice Smith", date := "...")]
@[transcriber (value := "Robert Jones", date := "...")]
@[title (lang := "en", value: = "the natural language name of theorem")]
@[title (lang := "fr", value := "le nom en langage naturel du théorème")]
@[description (lang := "en", value := "...")]
@[description (lang := "fr", value := "...")]
theorem ...

Intellisense

With a mathematical metadata ontology, a special key, chord, or sequence could enable Intellisense-integrated natural-language search.

That is, users could type a key, chord, or sequence to commence a text-entry mode where they could type a natural-language title (e.g., @[title] attributes), possibly then making use of an on-screen menu (e.g., showing items' @[title] and @[description] attributes' values), and/or press the Tab key to select a recommendation, to retrieve a Lean object identifier which would be entered into the Lean content.

Tooltips

With a mathematical metadata ontology, a @[description] attribute and perhaps @[example] attributes could be used to provide that content to display when a user hovers over a thing in VS Code. There could also be multiple types of descriptions, one being intended for search, the other for tooltips.

Alternatively, special-purpose attributes, such as @[tooltip] or @[usage], could be provided.

In addition to using attributes' text values, attributes could refer to functions which return text strings. For the use case of tooltips, perhaps such functions could receive data about the hovered-over thing and the hover event context.

Illustrations and Animations

See also: Lean widgets

Illustrations can enhance the comprehension of proofs by both human mathematicians and multimodal AI systems.

@[illustration ...]
theorem ...

Approaches considered here include (1) referring to visual content by relative or absolute URLs via a href, (2) using encapsulated visual templates which could receive arguments with which to produce visual content, and (3) fully procedurally-generated visual content where Lean functions would be able to receive arguments with which to vary resultant visual content (drawing with Lean).

With respect to producing illustrations for LaTeX documents, software options include [1]: PGF/TikZ, PSTricks, and the default graphics packages. Other graphics packages included in LaTeX include: pgfplots, Xy-pic, ePiX, MetaPost, MetaFun, and Mfpic. Independent GUI wrappers and software tools which create images suitable for inclusion in LaTeX documents include: LaTeXPiX, TPX, Xfig, Asymptote, Inkscape, Ipe, Knitr/Sweave, KtikZ,QtikZ, and GeoCobra.

Document Processing

Software for processing Lean content into other formats (e.g., markdown, wikitext, LaTeX, HTML, PDF, or Jupyter notebooks) could use attributes to provide features specific to the resultant output formats. For instance, some @[illustration] attributes could be used to obtain visual content to add to resultant output content.

Conclusion

Thank you for any comments, questions, or feedback on these ideas.

[nomeata]

Thanks for sharing these ideas! I agree that there are so many possibilities for extending code with auxillary information, visual representation etc.

What I'm missing from this RFC though is a very strong motivation to create these as built-in attributes. Lean is very extensible in particular to allow such features to be developed outside the core component. For something with a vast design space as these, I would feel more comfortable of such features are prototyped in their own library, maybe used to good effect within some larger development (maybe mathlib), and only when and if that proves to be useful we can consider making them official and out-of-the-box. Does that make sense?

[AdamSobieski]

Thank you. Yes, that makes sense.

With respect to the first subtopic of creating or selecting a mathematical metadata ontology to benefit search, Intellisense, and tooltips, in my opinion, a direct process towards including a resultant set of attributes in either core Lean or mathlib would be useful because, to showcase and deliver any benefits, any resultant set of attributes would need to be recognized by a number of other Lean projects: the Loogle search engine and the VS Code extension.

With respect to the second subtopic, illustration- and animation-related attributes, I included those ideas in this RFC while thinking about the automatic generation of educational multimedia documents from formal proofs. Yes, these ideas and uses of attributes could more readily be independently researched, developed, and prototyped with user libraries to showcase their uses and benefits before seeking to make any involved attributes official or out-of-the-box.

What do you think about that motivation for the first subtopic?

[nomeata]

Good points. Remember that core lean is not math specific, and most math results are in mathlib only. A mathematical ontology would, I expect, achieve all it can even if it lives in mathlib only - so maybe bring it up there? (The two projects are maintained and governed rather differently, and an RFC here will likely not lead to action on the mathlib side.)

Once the ontology exists there and is used by mathlib specific tools, I expect more general tools (Loogle, documentation) may begin to support it, or provide extension hooks necessary for it.

[AdamSobieski]

Excellent. Ok, I will revise and expand on this RFC, being sure to include a section for motivation, into a new issue for the mathlib4 community repository upcoming.

Thank you for mentioning documentation. I will include that in that issue's list of use cases.

[blokhin]

Dear @AdamSobieski, what is the mathematical metadata ontology in this context? Does it have anything to do with the semantic web ontologies (OWL, LISP) and logical reasoning on top of them?

[AdamSobieski]

@blokhin, hello. I've continued on these ideas in another issue: leanprover-community/mathlib4#15509 .

The issue, there, lists the use cases of automatically generating educational resources and documentation, enhancing the Loogle search engine, and enhancing developer experiences (Intellisense, tooltips). It may be the case that even more metadata attributes would make sense to broach for consideration with respect to the Lean ecosystem – for inclusion in the mathlib library – for those or more use cases.

In addition to attributes' properties being capable of having numbers or text strings for their values, other Lean elements could be referenced. For instance, if example elements could be optionally labeled or identified, theorem elements could be annotated with @[usage] attributes referencing those example elements which illustrate their usage.

Yes, developers could use Semantic Web technologies to perform reasoning over and to query metadata on Lean elements. In these regards, perhaps a @[uri] attribute would be useful for creating mappings between Lean elements and URIs.