ABSTRACT. Everyone who ever formalised an informal pen-and-paper proof is familiar with the annoying fact that the formal proof tends to be several times lengthier, more detailed, and more painful than the original informal one. In the first half of this talk I will present some of my thoughts on what contributes to this, and specific examples of how the problem can be (and successfully been) mitigated in Isabelle/HOL. In the second half, I will talk more concretely about one particularly striking example: a domain-specific automation tool to solve problems related to the asymptotics of real-valued functions.

ABSTRACT. The Gromov-Hausdorff space is usually defined in textbooks as ``the space of all compact metric spaces up to isometry''. We describe a formalization of this notion in the Lean proof assistant, insisting on how we need to depart from the usual informal viewpoint of mathematicians on this object to get a rigorous formalization.

ABSTRACT. We report on our experience formalizing differential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this effect, we stress the possibly surprising difference between the formalization and its pen-and-paper counterpart arising from Lean's treatment of equality. Our three case studies are Lie groups, vector bundles and the Lie algebra of a Lie group.

ABSTRACT. Formal proof is regarded as an insufficient alternative to informal proof because it has both advantages and disadvantages, compared to informal proof. Focusing on the macro structure of proof, this study proposes assimilating the structure of formal proof and informal proof to retain both readability and verifiability. An implementation example of the Ntac system, a library for the Lean theorem prover, is introduced. The system converts Lean script into natural language text, which allows treating formal proof as informal proof.

ABSTRACT. We present two formalizations with the natural proof assistant Naproche which explore the notational and typographical potential of the new LaTeX input format. The first formalization leads up to Yoneda’s Lemma in category theory. Commutative diagrams are defined and printed using the LaTeX package tikz-cd. A specific Naproche module translates a commutative diagram defined by tikz-cd commands into equalities of functional compositions which are proved by the Naproche reasoner. The second formalization is an abstract version of Euclid’s proof of the infinitude of primes, using general algebraic concepts. It uses LaTeX commands to follow the common mathematical practice of making some obvious symbols implicit and hide them from the typeset output. The hidden information can be revealed by hovering over the pdf-output.

ABSTRACT. Rotation number is the key numerical invariant of an orientation preserving circle homeomorphism. This paper describes the current state of an ongoing project with aim to formalize various facts about circle dynamics in Lean. Currently, the formalized material includes the definition and basic properties of the translation number of a lift of a circle homeomorphism to the real line. I also formalized a theorem by É.~Ghys that says that two actions of a group on a circle by homeomorphisms are semi-conjugate provided that for some lifts of these actions to the real line, corresponding maps have equal translation numbers.

ABSTRACT. In this paper, we report on developing a web platform for hosting the Mizar Mathematical Library (MML). As the size of formalized mathematical libraries has been drastically increasing in recent years, there has been a growing demand for tools that support efficient and comprehensive browsing and searching of those libraries. A Wiki function for adding comments to the HTMLized MML and three types of search functions (article name, symbol name, and theorem) are implemented in this platform. It is also designed to maintain consistency during library updates by using Git as its backend. This platform aims at long-term use, with the highest priority on usability, extendability, and interoperability. We are planning to add features such as a dependency graph component in the future.

ABSTRACT. Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses are used by \mathlib for scalar actions with examples, illustrate some of the problems which come up when using them such as compatibility of actions and non-definitionally-equal diamonds, and note how these problems can be solved. We outline where more work is needed in \mathlib in this area.

ABSTRACT. When producing large formally verified mathematical developments that make use of typeclasses it is easy to introduce overly strong assumptions for theorems and definitions. We consider the problem of recognizing from the elaborated proof terms when typeclass assumptions are stronger than necessary. We introduce a metaprogram for the Lean theorem prover that finds and informs the user about possible generalizations.

ABSTRACT. The campaign to transform traditional mathematical practice into a formal discipline appears to have been a great success.  Several sophisticated proof assistants have been developed, a great deal of mathematical knowledge has been formalized, a growing number of researchers in computing and mathematics are now using proof assistants to check the theorems they prove, and a new area of computing called formal methods has been established in which formal mathematics is used in the development of hardware and software.  However, the campaign has largely been a failure when viewed from a broader perspective.  It has had almost no impact on mathematical practice.  Far less than 1% of all mathematics practitioners have ever used a formal logic or a proof assistant in their work.  We propose an alternative approach to formal mathematics that is characterized by (1) proofs are written in a traditional (nonformal) style, (2) the underlying logic is as close to mathematical practice as possible, (3) mathematics is organized in accordance with the little theories method as a theory graph, and (4) supporting software systems are easy to build and use.  We have begun a research program called Formal Mathematics for the Masses to make formal mathematics more useful, accessible, and natural to a wider range of mathematics practitioners by implementing this alternative approach.

ABSTRACT. We present an ongoing and future (partial re-)implementation of sTeX, a LaTeX package for semantic markup of mathematical documents.

ABSTRACT. In this extended abstract, we report on our ongoing work on the automated translation of high-school geometry statements into a formal language of syntax trees in first-order logic. We see this as the first step before translating both statements and proofs, and before widening the scope to parsing natural language mathematics in general. Our approach is based on Arsenal, a framework developed at SRI International for building domain-specific semantic parsers translating natural language to structured representations, namely expression trees. Arsenal trains a model (in this case, a sequence-to-sequence model) from synthetic datasets that it generates from the grammar of expression trees that it targets, which is particularly useful for domains where ground truth data is sparse or even nonexistent.