ABSTRACT. Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, adaptability, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes.
ABSTRACT. This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions.
ABSTRACT. GeoGebra Discovery is an experimental version of GeoGebra, dealing with automated reasoning in elementary geometry. It contains some bleeding edge features of GeoGebra that are under heavy development and therefore not intended for every day use yet, so they are not included in the official GeoGebra version. Also, in some cases, there is no consensus on whether to include certain elements in GeoGebra or to leave them out (for example, because they are too specific for a particular audience).
GeoGebra Discovery is maintained by a group of researchers from various fields of interest, including mathematics education, algebraic geometry and computer science.
ABSTRACT. To cater to the increasingly diverse student bodies, higher education has to personalize education. In times of stagnant educational budgets and staffing problems, this can only be achieved via adaptive, interactive learning support services. In this paper we show how these can be generated by modeling the domain, the learner competencies, and the rhetoric and didactic relations among learning objects, re-using existing technologies and systems of mathematical knowledge management.
ABSTRACT. This paper outlines our ideas of how to teach linear algebra
in a mechanized mathematical environment, and discusses some of our
reasons for thinking that this is a better way to teach linear algebra
than the “old fashioned way.” We discuss some technological tools such
as Maple, Matlab, Python, and Jupyter Notebooks, and some choices
of topics that are especially suited to teaching with these tools. The
discussion is informed by our experience over the past thirty or more
years teaching at various levels, especially at the University of Western
Ontario.
ABSTRACT. When publishing papers, researchers in mathematics and related disciplines
typically focus on the presentation, i.e. type-setting, of their ideas and
provide little semantic information. This impedes the development of services
that benefit from semantic information, such as semantic search and screen
readers for vision-impaired researchers. As a remedy, there have been attempts
to infer semantic data from already published papers using small programs that
we call spotters. Unfortunately, there is no standardized format for semantic
annotations and spotter authors typically invent their own format. This leads
to two problems: i) there is no ecosystem of tools for common tasks like the
visualization of results or the manual annotation of a gold standard, and ii)
re-using, evaluating and combining results becomes very difficult.
In this paper, we address the issue by describing a standardized, flexible way
to represent semantic annotations, using semantic web technologies and, in
particular, the web annotation standard. Furthermore, we describe SpotterBase,
a set of tools to help with processing the annotations and creating new ones.
ABSTRACT. Mathematical formulae are a significant challenge for various services
that help us access scientific publications. For example, finding relevant
formulae with a search engine is difficult and screen readers struggle
to verbalize them in an understandable way. We believe that such
services could be improved if more semantic information is available.
To automatically extract this information, we typically need manually
annotated data sets for evaluation and, potentially, for the training of
machine learning models. However, mathematical formulae also present
a major challenge for annotation tools, as they cannot be presented well
as plain text which is required by most existing tools. In this context,
we present AnnoTize, a new annotation tool. It can create, display
and update annotations for HTML5 documents and was specifically
designed to support the fine-grained annotation of formulae encoded in
MathML. As manual annotation can be tedious and time-consuming,
AnnoTize offers several features to speed up the annotation process for
large annotation tasks.
ABSTRACT. This paper discusses the enhancements we have made to the Mizar Extension for Visual Studio Code (VSCode). The first part of the paper explores the creation of the Mizar Server and client-side infrastructure, developed to support the web version of the Mizar Extension for VSCode. The latter part provides an update on the development of the formatter function and reports on the progress of our research into coding assistance using ChatGPT.
ABSTRACT. We extract mathematical concepts from mathematical text using generative large language models
(LLMs) like ChatGPT, contributing to the field of automatic term extraction (ATE) and mathematical text processing, and also to the study of LLMs themselves.
Our work builds on that of others, %especially~\cite{collard2022},
in that we aim for automatic extraction of terms (keywords) in one mathematical field, category theory, using as a corpus the 755
abstracts from a snapshot of the online journal \emph{Theory and Applications of Categories}, circa 2020. Where our study diverges
from previous work is in
(1) providing a more thorough analysis of what makes mathematical term extraction a difficult problem to begin with;
(2) paying close attention to inter-annotator disagreements;
(3) providing a set of guidelines which both human and machine annotators could use to standardize the extraction process;
(4) introducing a new annotation tool to help humans with ATE, applicable to any mathematical field and even beyond mathematics;
(5) using prompts to ChatGPT as part of the extraction process, and proposing best practices for such prompts;
and (6) raising the question of whether ChatGPT could be used as an annotator on the same level as human experts.
Our overall findings are that the matter of mathematical ATE is an interesting field which can benefit from participation by LLMs,
but LLMs themselves cannot at this time surpass human performance on it.
Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk)
ABSTRACT. An attractive and powerful method for organizing mathematical knowledge is the little theories method [5]. A body of mathematical knowledge is represented in the form of a theory graph [7, 8] consisting of theories as nodes and theory morphisms as directed edges. Each mathematical topic is developed in the “little theory” in the theory graph that has the most convenient level of abstraction and the most convenient vocabulary. Then the definitions and theorems produced in the development are transported, as needed, from this abstract theory to other, usually more concrete, theories in the graph via the theory morphisms in the graph. Alonzo [4] is a practice-oriented classical higher-order logic. Named in honor of Alonzo Church, Alonzo is based on Church’s type theory [1], Church’s formulation of simple type theory [3]. Unlike traditional predicate logics, Alonzo admits partial functions and undefined expressions in accordance with the approach employed in mathematical practice that we call the traditional approach to undefinedness [2]. Alonzo has a simple syntax with a formal notation for machines and a compact notation for humans that closely resembles the notation found in mathematical practice. It has two semantics, one for mathematics based on standard models and one for logic based on Henkin-style general models [6]. By virtue of its syntax and semantics, Alonzo is exceptionally well suited for expressing and reasoning about mathematical ideas in a natural manner. Alonzo is also equipped with a set of mathematical knowledge modules for constructing theories and theory morphisms and for transporting definitions and theorems from one theory to another via theory morphisms. This talk illustrates the little theories method by showing how to formalize a sample body of mathematical knowledge in Alonzo as a theory graph using Alonzo’s mathematical knowledge modules. We have chosen monoid theory as the sample body of mathematical knowledge. A monoid is an algebraic structure consisting a nonempty set, a total, associative binary function on the set, and a member of the set that is an identity element 1 with respect to the function. Monoids are abundant in mathematics and computing. Our formalization of monoid theory in Alonzo consists of a theory graph containing 12 theories and 24 theory morphisms. Instead of the standard certification-oriented approach to formal mathematics, we follow a communication-oriented approach that (1) is fully formal except proofs are written in a traditional (informal) style and (2) priorities the communication of mathematical ideas over the formal certification of mathematical results.
References
[1] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
[2] W. M. Farmer. Formalizing undefinedness arising in calculus. In D. A. Basin and M. Rusinowitch, editors, Automated Reasoning — IJCAR 2004, volume 3097 of Lecture Notes in Computer Science, pages 475–489. Springer, 2004.
[3] W. M. Farmer. The seven virtues of simple type theory. Journal of Applied Logic, 6:267–286, 2008.
[4] W. M. Farmer. Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas. Computer Science Foundations and Applied Logic. Birkhauser, 2023.
[5] W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In D. Kapur, editor, Automated Deduction — CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567–581. Springer, 1992.
[6] L. Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15:81–91, 1950.
[7] M. Kohlhase. Mathematical knowledge management: Transcending the one-brain-barrier with theory graphs. European Mathematical Society (EMS) Newsletter, 92:22–27, June 2014. [8] M. Kohlhase, F. Rabe, and V. Zholudev. Towards MKM in the large: Modular representation and scalable software architecture. In S. Autexier, J. Calmet, D. Delahaye, P. D. F. Ion, L. Rideau, R. Rioboo, and A. P. Sexton, editors, Intelligent Computer Mathematics, volume 6167 of Lecture Notes in Computer Science, pages 370–384. Springer, 2010.
ABSTRACT. Mathematics is made up of a vast web of interrelated concepts and definitions. To successfully formalize a proof, a mathematician must first possess a deep understanding of the concepts involved. As mathematical knowledge continues to expand in both breadth and depth, it is becoming increasingly challenging for individual mathematicians to be fluent in multiple areas of mathematics. MathGloss seeks to partially address this issue by creating a unified framework for organizing and accessing mathematical concepts, enabling individuals to effortlessly navigate and comprehend them.
Concepts in mathematics are delineated by their definitions, and yet these definitions may take different forms depending on the context in which they are used. Notably, definitions in the proof assistant Lean look very different from the definitions found in undergraduate math textbooks. By gathering and connecting different definitions of the same concept from different sources, we hope to enable both novice and seasoned mathematicians to unify their understanding of basic concepts with an eye to formalization. This is done from several corpora as follows:
From “Chicago Notes,” we have more than 500 definitions curated by an undergraduate student from the courses she took at the University of Chicago.
From “France,” there are approximately 300 terms from the French undergraduate curriculum in mathematics as translated by the Lean Community [1]. Some of these terms have direct links to items in Lean, and they are included where they already exist.
From "Maths Dictionary," there are 246 terms linked manually both to Wikidata and a French-language translation by Tim Hosgood [2].
From "nLab," there are approximately 5,000 terms from page titles of the online mathematics wiki called nLab [3] with people, books, and other non-concepts removed as best as we are able. These terms are linked to their pages in the nLab.
The collected terms are mapped to Wikidata [4], the database that serves Wikipedia and many other knowledge projects using a tool called wikimapper [5]. This enables us to match together concepts appearing in several of our corpora together and achieve our goal of combining different sources of information about the same objects. While some terms from the corpora do not have representations in Wikidata at the moment, the majority do and we aim to get as many of these as possible. In short, we combine mathematical concepts with natural mathematical language describing them, with their representations in a well-established knowledge ontology, and with their representations in Lean.
The database can be found at https://mathgloss.github.io/MathGloss/. It is intended to be updated easily to include definitions from other sources like the Encyclopedia of Mathematics, Wolfram MathWorld, or PlanetMath. These also have glossaries, but MathGloss is unique in that it provides an overarching view of multiple sources.
Such organization of information is essential if mathematics is to embrace formalization as a useful tool for practice and for education [6]. Given that a proof assistant will “complain that it does not understand the definitions, axioms, or reasoning steps entered by the mathematician,” MathGloss should prove useful for bridging the gap between brain and computer.
ABSTRACT. The latest release of the natural language proof assistant Naproche [1], developed at the university of Bonn, Germany, which ships as a component of the current Isabelle release [2,3] comprises new foundational libraries about set and number theory.
The Naproche (“Natural Proof Checking”) proof assistant is being developed for a high degree of naturalness of accepted proof texts, written in the controlled natural language ForTheL (“Formula Theory Language”). ForTheL is designed to approximate the mathematical vernacular, while at the same time being a completely formal language which allows its translation into formal logics [4]. Naproche has a built-in softly typed ontology that can be regarded as a weak fragment of Kelley–Morse set theory. While this ontology can quite flexibly be extended by a user, it does not provide a sufficient basis on its own to formalize sophisticated mathematics. To overcome this issue, Naproche also provides three foundational libraries about set and number theory on top of its built-in ontology [5]:
One library that provides basic set-theoretical notions and operations as well as the most commonly used Kelley–Morse axioms [6].
One that extends the first library with more advanced notions from set theory like that of ordinal and cardinal numbers [7].
One that extends the first library with a new (soft) type of natural numbers together with common arithmetical operations as well as some basic notions of number theory [8].
Since these libraries are written in a LaTeX dialect of ForTheL they not only comprise a high degree of human readability but can also be converted directly to PDF. Moreover, their applicability as practically usable foundations for more advanced formalizations in Naproche is demonstrated by using them as a basis for formalizations of some well-known theorems from set and number theory that ship with Naproche, e.g. the Cantor-Schroeder-Bernstein theorem [9,10] and Furstenberg's proof of the infinitude of primes [11,12]. However, they also pose some serious problems yet that have to be addressed in future versions of Naproche:
Modularity: Since Naproche lacks a mature module system for organizing formalizations, their reusability is currently fairly limited.
Scalability: The proof checking abilities of Naproche do not scale well with the size of the libraries.
Time redundancy: Currently Naproche has no mechanisms to provide persistent certificates of the correctness of its libraries so they are rechecked by the system every time they are imported to a ForTheL document.
Abstract mathematical structures: Naproche's current abilities of handling abstract mathematical structures (such as groups or topological spaces) in contrast to “concrete” ones like "the" universe of sets or “the” structure of natural numbers are very limited. This demands for an extension of ForTheL that can handle such abstract structures using language constructs that do not differ remarkably from the mathematical vernacular.
Hence, although Naproche appears as a promising basis for dealing with human-readable, formal mathematical libraries, there is much room for further improvement of its capabilities using methods developed in the 'intelligent computer mathematics' community.
[3] De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Wenzel, M. (2021). The Isabelle/Naproche Natural Language Proof Assistant. In: Platzer, A., Sutcliffe, G. (eds) Automated Deduction – CADE 28. CADE 2021. Lecture Notes in Computer Science(), vol 12699. Springer, Cham. https://doi.org/10.1007/978-3-030-79876-5_36
[4] De Lon, A., Koepke, P., Lorenzen, A., Marti, A., Schütz, M., Sturzenhecker, E. (2021). Beautiful Formalizations in Isabelle/Naproche. In: Kamareddine, F., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2021. Lecture Notes in Computer Science(), vol 12833. Springer, Cham. https://doi.org/10.1007/978-3-030-81097-9_2
[5] Schütz, M., De Lon, A., Koepke, P. (2022). Setting up Set-Theoretical Foundations in Naproche. In: Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings). https://www3.risc.jku.at/publications/download/risc_6584/proceedings-CICM2022-informal.pdf
ABSTRACT. Proving the details required for formal proofs in Category Theory is often tedious. This is made worse when using E-Category Theory, as is often found in proof-assistant libraries for category theory today[1]: a destination often called "Setoid Hell". It is even worse when using P-Category Theory[2] (a variant of E-Category Theory where Partial Equivalence Relations are used), which is required for our work: a new destination of "Subsetoid Hell". This short talk will present how structuring the proof of the presheaf exponential in a more categorical fashion allows some of this tedium to be reduced (although, not completely eliminated). This also results in a fuller library of categorical results shedding new light on P-category theory, and allowing for improved future development. However, the grass is not completely greener when proofs are more categorical: the proof terms are often worse and less computationally efficient. Techniques to overcome this seem to force a mild return to Hell.
All the work presented is formalized in the Coq Proof Assistant. This is a crucial aspect of the research programme where constructiveness and computability of the formalized proof is a motivating property.
[1] Jason Z. S. Hu and Jacques Carette. 2021. Formalizing Category Theory in Agda. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (Virtual, Denmark) (CPP 2021). Association for Computing Machinery, New York, NY, USA, 327–342. https://doi.org/10.1145/3437992.3439922
[2] Djorde Čubrić, Peter Dybjer, and Philip Scott. 1998. Normalization and the Yoneda Embedding. Mathematical Structures in Computer Science 8, 2 (apr 1998), 153–192. https://doi.org/10.1017/S0960129597002508
