ABSTRACT. We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general and builds on developments in linear algebra, analysis, measure theory, and descriptive set theory. The interplay between these domains is transparent thanks to the highly integrated development model of mathlib.

ABSTRACT. When evaluating or simplifying mathematical expressions, the question arises of how to handle inverse functions. The problem is that for a non-injective function $f: D \rightarrow R$, the inverse is generally not a function $R \rightarrow D$ since there may be multiple pre-images for a given point. The majority of work in this area has fallen into two camps: either the inverse functions, and expressions involving them, are treated as multi-valued objects, or inverse functions are taken to have one principal value. Both these approaches lead to difficulties in evaluation and simplification. It is possible to define the inverse as a function from $R$ to sets of elements of $D$, but then the algebra of expressions involving the inverse becomes overly complicated. This article extends previous work based on a different approach: instead, the inverse of a function is taken to be a labelled family of functions, with the label specifying the pre-image in the original function's domain. This convention is already used by some authors for logarithms, but it can be applied more generally. In some cases, the branch indices can appear in identities that give more broadly applicable simplification rules. In this paper we survey how this approach can be applied to elementary functions, including the Lambert W function, and give examples using Maple.

ABSTRACT. This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments to the HTMLized MML, three types of search function (article, symbol, and theorem), and a function to show the dependency graph of the MML. This platform is designed with consistency, scalability, and interoperability as top priorities for long-term use.

ABSTRACT. We report on sTeX3 – a complete redesign and reimplementation (using LaTeX3) from the ground up of the sTeX ecosystem for semantic markup of mathematical documents. Specifically, we present: i) The sTeX package that allows declaring semantic macros and provides a module system for organizing and importing semantic macros using logical identifiers. sTeX3 is a (now) standard LaTeX package with minimal dependencies and is compatible with arbitrary document classes and packages. ii) The RusTeX system, an implementation of the core TeX-engine in Rust, that allows for converting arbitrary LaTeX-documents to XHTML. It allows for converting arbitrary LaTeX-documents to XHTML -- for sTeX3-documents enriched with semantic annotations based on the OMDoc ontology iii) An MMT integration: The RusTeX-generated XHTML can be imported and served by the MMT system for further semantic knowledge management services.

ABSTRACT. The paper presents the sTeX3 format for representing informal mathematics. sTeX3 acts as a surface language for two systems: the (presentation-oriented) LaTeX system to produce PDF and the semantics-aware MMT system for advanced knowledge management services. We discuss how the sTeX3 markup facilities allow in situ flexiformalization (and the necessary elaboration of complex structures), while staying presentationally neutral.

ABSTRACT. We present a formalisation of basic topology in simple type theory encoded using the Isabelle/HOL proof assistant. In contrast to related formalisation work, which follows more 'traditional' approaches, our work builds upon closure algebras, encoded as Boolean algebras of (characteristic functions of) sets featuring an axiomatised closure operator (cf. seminal work by Kuratowski and McKinsey \& Tarski). With this approach we primarily address students of computational logic, for whom we bring a different focus, closer to lattice theory and logic than to set theory or analysis. This approach has allowed us to better leverage the automated tools integrated into Isabelle/HOL (model finder Nitpick and Sledgehammer) to do most of the proof and refutation heavy-lifting, thus allowing for assumption-minimality and less-verbose interactive proofs.

ABSTRACT. Partial Differential Equations (PDEs) are widely used for modeling the physical phenomena and analyzing the dynamical behavior of many engineering and physical systems. The heat equation is one of the most well-known PDEs that captures the temperature distribution and diffusion of heat within a body. Due to the wider utility of these equations in various safety-critical applications, such as thermal protection systems, a formal analysis of the heat transfer is of utmost importance. In this paper, we propose to use higher-order-logic (HOL) theorem proving for formally analyzing the heat conduction problem in rectangular coordinates. In particular, we formally model the heat transfer as a one-dimensional heat equation for a slab using the multivariable calculus theories of the HOL Light theorem prover. This requires the formalization of the heat operator and the formal verification of its various properties, such as linearity and scaling. Moreover, we use the separation of variables method for formally verifying the solution of the Partial Differential Equation (PDE) modeling the heat transfer under various initial and boundary conditions using HOL Light.

ABSTRACT. In 1964, Paul Erdős published a paper settling a question about function spaces that he had seen in a problem book. Erdős proved that the answer was yes if and only if the continuum hypothesis was false: an innocent-looking question turned out to be undecidable from the axioms of ZFC. The formalisation of these proofs in Isabelle/HOL demonstrate the combined use of complex analysis and set theory, and in particular how the Isabelle/HOL library for ZFC integrates set theory with higher-order logic.

ABSTRACT. Counting the solutions of symbolic encodings is an intriguing computational problem with many applications. In the field of propositional satisfiability (SAT) solving, for example, many algorithms and tools have emerged to tackle the counting problem. For quantified Boolean formulas (QBFs), an extension of SAT with quantifiers used to compactly encode problems of formal verification, synthesis, planning, etc., practical solution counting has not been considered yet.

We present the first practical counter of top-level solutions, i.e., a tool for counting full assignments of the variables in the outermost quantifier. Our tool is able to count such solutions for true and for false formulas.

ABSTRACT. Nondeterministic finite automata (NFAs) are an important model of computation. The equivalence problem for NFAs is known to be PSPACE-complete, and several specialized algorithms have been developed to solve this problem. In this paper, we approach the equivalence problem for NFAs by means of another PSPACE-complete problem: quantified satisfiability (QSAT). QSAT asks whether a quantified Boolean formula (QBF) is true. We encode the NFA equivalence problem as a QBF which is true if and only if the input NFAs are not equivalent. In addition to determining the equivalence of NFAs, we are also able to decode strings that witness the inequivalence of two NFAs by looking into the solving certificate. This is a novel application of certified QSAT solving. The encoding is formally verified in the Isabelle/HOL theorem prover.

ABSTRACT. This work discusses the mechanisation in Isabelle/HOL of a general version of Hall's Theorem. It states that an enumerable family of finite sets has a system of distinct representatives (SDR) if it satisfies the ``marriage condition''. The marriage condition states that every finite subfamily of the possible infinite family of sets contains at least as many distinct members as the number of sets in the subfamily. The proof applies a formalisation of the Compactness Theorem for propositional logic. It checks the marriage condition for finite subfamilies of sets using Jiang and Nipkow's formalisation of the finite version of Hall's Theorem.