Semantic annotations enable services that make the knowledge in documents more accessible. In the case of ALeA, an adaptive learning assistant we use as a case study, they enable, for example, guided tours and practice problems tailored to the learner's competencies. However, the cost of semantic authoring is substantial and tool support is limited. In this paper we discuss the nature of the semantic authoring task and argue that, while sharing aspects of both classical (informal) authoring and formal authoring, it is a task of its own that needs special editing support facilities. We present and evaluate a simple utility that supports the process of annotating technical terms with semantic references to a flexiformal content commons and increases annotation productivity by almost an order of magnitude.
The effort required for maintaining large libraries of formal mathematics is quite substantial. In this work, we exploit structural similarity to alleviate the burden of maintenance, investigating two main problems: First, we present a general framework for detecting duplicates in large libraries of formal mathematics, combining surface-level syntax, document markup, and the underlying formulae. For scalability, we generate potentially matching candidates with a discriminator-based approach. On Isabelle/HOL, our method maintains perfect precision up to a similarity threshold of 0.95. Secondly, we address the issue of out-of-place auxiliary lemmas that are frequently created during development of indepth formalizations. We propose a community detection approach on the underlying dependency graph of formal entities, which finds co-located lemmas that have similar link patterns. For a dataset of lemmas moved during Isabelle development, the correct location is in the top 6 neighborhoods suggested by our approach on average (median).
During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries. Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.
Flexible Boolean semantics is a framework for analysing natural language using Boolean algebras and flexibility principles. In this article, we use flexible Boolean semantics to analyse the language of mathematics. We find that the framework cannot be used to produce desirable results for sentences in which the subject is a coordination of definite descriptions, each denoting a set, and the predicate describes a property of sets. To resolve this issue, we extend the type system and the operators from the framework to handle such sentences.
Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this article, we propose a new learning environment as a layer above the Lean proof assistant, specifically targeting high-school level proofs. Drawing inspiration from coherent logic and adaptations of proof assistants for teaching, such as Lean-Verbose and Coq Waterproof, along with our own experience using proof assistants in higher education, we designed Yalep, a declarative controlled natural language, with a minimal number of syntactic constructions, which favors forward-chaining of facts. Yalep provides convenience for type theory hiding, and functions defined on type subsets. This paper presents the design choices and implementation of these features.
Flexiformal documents – i.e. documents with embedded semantic annotations that make some aspects of their content machineactionable – can be instrumented to make interaction with the underlying knowledge more efficient and effective. Fostering such interactions via semantic services has proven very successful in university education, but the practical applicability is limited by the cost of flexiformalization. A method for lowering (flexi)-formalization costs is to use modular representations to profit from enhanced source sharing and induced (generated) content. In fully formal environments this is well-understood and implemented in many systems. In this paper we show that many of the formal techniques carry over to the informal setting if we parse (rigorous) natural language with a semantically optimized grammar and work on abstract syntax trees instead of formulae. We present i) a set of use cases for generating learning material to be used in an educational setting – concretely in the field of theoretical computer science, ii) a GF grammar that allows to syntactically analyze the underlying language fragment, iii) a set of AST-to-AST simplifications that can be used to fine-tune the wording and formulae of the generated content and adapt it to the scientific jargon, and iv) a prototypical implementation that shows the technique in action.
In 1956, Robert M. Solow published a mathematical theory which describes capital accumulation, technological advancements, and population growth. The Solow model is widely used in economics. In this paper we describe a formalization of the model in the ℕ aproche proof assistant. The formalization also encompasses mathematical foundations from real analysis. This is the first formalization of an economic model which is also readable like an ordinary mathematical text.
Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative ( ), commutative ( 𝙲 ), and associative-commutative ( 𝙰𝙲 ) equational theories. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests modulo theories within the equivariance algorithm.
Social choice theory is a multidisciplinary research area that studies collective decision-making based on individual preferences. A central problem in this domain is the fair assignment of indivisible resources, which arises in applications such as organ matching, school admissions, and job placements. Notions of fairness, such as proportionality and envy-freeness, are well-established; they are sometimes unattainable, particularly in the discrete setting, where resources cannot be divided. We present a mechanised formalisation of key fairness concepts for the assignment problem under ordinal preferences using the Isabelle/HOL theorem prover. Our development captures both discrete and fractional assignment settings and formalises the responsive set extension, which is a central concept for lifting preferences over resources to preferences over sets of resources, enabling the comparison of allocations under ordinal preferences. We formalise multiple fairness notions-including stochastic dominance (SD) proportionality and envy-freeness, as well as their relaxed variants-and we formally verify relationships between these notions. The formalisation builds on existing verified results in social choice theory and closes gaps found in pen-and-paper proofs.
Kofler's DynGenPar (DGP) generalized dynamic parsing algorithm [6,7] is aimed at parsing the language of mathematics. Notably, DGP uses a notion of initial graph instead of parsing tables in the style of GLR and LR parsers. We distinguish the two previously existing definitions of DGP: (1) The high-level "Abstract DGP" (ADGP) is a non-deterministic algorithm which reaches any particular parse tree via a sequence of non-deterministic choices. It is not obvious just from reading ADGP how to implement it well. (2) Kofler's C++ implementation (KDGP) implements its own concurrency engine for finding all possible parse trees simultaneously while synchronizing on each input token. It is challenging to comprehend how ADGP corresponds to KDGP, and it would be hard to formally prove properties of either ADGP or KDGP. We present a new mathematical definition of Core DGP (CDGP), the context-free grammar (CFG) core of DGP, that is both declarative and deterministic. We formalize the concurrency with a notion of continuation, and define a way to match continuations to parse trees in proving that our algorithm is sound and complete, i.e., it terminates and returns all valid parse trees excluding trees with superfluous recursion. We also make available a Python implementation which corresponds quite directly to the mathematical definition of CDGP.
Proof autoformalization aims to generate formal proofs from natural-language (NL) statements. While large language models (LLMs) show promise, they struggle with accuracy on complex proofs, and their size and cost limit broader use. We evaluate the LLM mistral-large -2411 on the Herald dataset, a large collection of aligned informal and formal Lean proofs. Our analysis reveals common model errors and structural issues in the dataset, including data leakage. Using iterative prompt refinement and practical fixes, we improve formalization quality. This work highlights both the potential and current limits of prompt-based autoformalization.
Dedukti and MMT are both examples of tools that can collect mathematical libraries coming from different systems in a unified but heterogeneous body. Indeed, both tools implement a logical framework where the logics or type systems of the various mathematical assistants can be represented, so that their libraries can be encoded in a single format preserving well-typedness. Still, the images of the various libraries remain disjoint: logical consistency of their union is not granted, the encoding of the various statements differs from logic to logic, and the same mathematical entity remains defined repeatedly and independently. To benefit from the common representation, then, additional tools need to be developed, for example, to translate results encoded in the representation of a logic into the representation of a stronger logic, taking care of aligning the duplicated mathematical entities. In this paper we address the challenges posed by indexing and searching the large, heterogeneous library. For example, users may expect to find results in the library up to the encoding used and up to alignments, so to be able to mix in the search result statements originally coming from different systems and logics. In particular, we describe new indexing and retrieval capabilities that we integrated directly into the LambdaPi proof assistant, that can work on Dedukti files.
Large Language Models (LLMs) have shown impressive capabilities in solving complex mathematical problems, making them valuable tools for education, research, and automated tutoring. However, top-performing models on benchmarks like MATH500, such as GPT-4 and DeepSeek-R1, are often large, proprietary, and costly to use, limiting their accessibility. In contrast, smaller open-source models are more affordable and easier to deploy locally but typically underperform in mathematical reasoning tasks. In this work, we explore the math-problem-solving potential of six small-scale, open-source LLMs (all under 10 billion parameters): Arithmo-Mistral-7B, MAmmoTH-7B, MAmmoTH-8B, MetaMath-7B, MetaMath-Llemma-7B, and MetaMath-Mistral-7B, on the MATH500 benchmark. To enhance their accuracy, we apply two “test-time” ensemble strategies: (1) Intra-model ensemble, where each model generates five independent outputs and the most frequent prediction is selected; and (2) Inter-model ensemble, where 2-level majority voting is performed: first at the intra-level, then across all the models in the ensemble. Our results show that the Intra-model ensemble consistently improves performance over individual runs, and combining outputs across models yields further gains. An ensemble of all six models achieves 38
We introduce UniFormal, a formal language for mathematical knowledge representation that continues the evolution of OpenMath and MMT. It is motivated by the lack of identifiers in these languages that exhibit the scoping behavior needed for, e.g., the fields in a record or the variables in a polynomial. Its core feature is a separation of identifiers and associated contexts into three levels: The global context maintains the usual toplevel declarations that can be imported across libraries and nested packages via qualified names. The local context maintains the usual α -renamable bound variables with narrow syntactic scope. The novel regional context sits in between these and maintains the identifiers of the current theory. A stack of regional contexts is used to allow for expressions that move between regions, e.g., when applying a theory morphism to transport an expression from one theory to another. We present a minimal language in this style, focusing on the general intuitions underlying the design. We anticipate it to be extended flexibly towards specialized aspects of mathematical knowledge such as programming languages or theorem provers to enable interoperability through their shared core concepts. This approach has already proved successful in the design and implementation of a UniFormal programming language.
This paper introduces a novel approach to vector graphics drawing by formalizing it within Category Theory (CT). Using the categorical programming paradigm, CT abstractions are interpreted as design patterns within Functional Programming (FP), bridging theoretical formalism and practical implementation. Building on Yorgey’s work, we represent diagrams as lists of graphical primitives, serving as a normal form for vector graphics. Diagrams are manipulated via graphical transformations (e.g., translation, rotation, scaling, color change) and list concatenation, which are modeled as an endofunctor F. This enables the construction of a free monad 𝕋≅ as a way to accumulate operations into expression trees lazily. We formalize graphical marks as abstractions over diagrams via slice categories, and vector graphics as values of the free monad 𝕋 over marks. Lastly, we introduce graphic expressions as a way to leverage F-algebras and F-coalgebras to construct complex graphics systematically. A prototype implementation in Lean demonstrates the applicability of our theory in a programming language based on dependent types, illustrating how categorical programming bridges the gap between mathematical abstraction and practical programming. An implementation in Julia is presented elsewhere.
This paper discusses the formalization in PVS of diverse proofs of the infinitude of primes. These proofs are developed using techniques from various areas of mathematics, including set theory, algebra, analysis, number theory, and topology. The availability of such a variety of proofs is helpful as a didactic resource, aiming to encourage mathematicians working in different areas to adopt interactive theorem provers as one of their everyday tools. The presented collection of formalizations follows the proofs selected by Erdös, Aigner, and Ziegler in their famous work “Proofs from THE BOOK,” namely those based on Fermat numbers, Mersenne numbers and algebraic structures, topological properties, and the analysis of harmonic series. The paper discusses the differences between informal proofs and mechanical formalization, highlighting the usefulness of distinguishing features of PVS to guide and facilitate the presented mechanization.
We use automated theorem provers to significantly shorten a formal development in higher order set theory. The development includes many standard theorems such as the fundamental theorem of arithmetic and irrationality of square root of two. Higher order automated theorem provers are particularly useful here, since the underlying framework of higher order set theory coincides with the classical extensional higher order logic of (most) higher order automated theorem provers, so no significant translation or encoding is required. Additionally, many subgoals are first order and so first order automated provers often suffice. We compare the performance of different provers on the subgoals generated from the development. We also discuss possibilities for proof reconstruction, i.e., obtaining formal proof terms when an automated theorem prover claims to have proven the subgoal.
Proofgold is a blockchain that supports formalized mathematics alongside standard cryptocurrency functionality. It incorporates logical constructs into the blockchain, including declarations of formal theories, definitions, propositions and proofs. It also supports placing and collecting bounties on proving these propositions, incentivizing the development of the formal libraries contained in Proofgold. In this paper, we present a web-based blockchain explorer for Proofgold. The system exposes not only the usual transactional data but also the formal mathematical components embedded in the chain and allows some interaction with them. The explorer allows users to inspect blocks, transactions, and addresses, as well as formal objects: theories, definitions, theorems and their proofs. We also support the submission of transactions to the blockchain using our interface. We describe the system architecture and its integration with the Proofgold Lava software, highlighting how the explorer supports navigation of formal content and facilitates mathematical knowledge management in a decentralized setting, as well as a number of formalizations in category theory done in the system.
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding maintainer overload. This includes dealing with breaking changes via a deprecation system, using code quality analysis tools (linters) to provide direct user feedback about common pitfalls, speeding up compilation times through conscious library (re-)design, dealing with technical debt as well as writing custom tooling to help with the review and triage of new contributions.
Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as ∀∃-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the ∀∃-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis.
