ABSTRACT. With more than 120.000 articles published annually in mathematical journals alone, mathematical search has often been touted as a killer application of computer-supported mathematics. But the artefacts of mathematics that should be searched are of very different natures such as mathematical documents, formulas, algorithms, concrete data sets, or semantic web--style graph abstractions. All are organized in complex ways and offer very different challenges and techniques for search. Therefore, existing representation languages and the corresponding query languages and search systems usually concentrate on only one of these aspects. As a consequence, each of these systems only partially covers the information needs of mathematical practitioners, and integrated solutions allowing multi-aspect queries are rare and basic. In this paper we present an architecture of a generic multi-aspect search system and evaluate it on paradigmatic examples of mathematical information needs.

ABSTRACT. We present the first release of OntoMathEdu, a new educational mathematical ontology. The ontology is intended to be used as a Linked Open Data hub for mathematical education, a linguistic resource for intelligent mathematical language processing and an end-user reference educational database. The ontology is organized in three layers: a foundational ontology layer, a domain ontology layer and a linguistic layer. The domain ontology layer contains language-independent concepts, covering secondary school mathematics curriculum. The linguistic layer provides linguistic grounding for these concepts, and the foundation ontology layer provides them with meta-ontological annotations. The concepts are organized in two main hierarchies: the hierarchy of objects and the hierarchy of reified relationships. For our knowledge, OntoMathEdu is the first Linked Open Data mathematical ontology, that respects ontological distinctions provided by a foundational ontology; represents mathematical relationships as first-oder entities; and provides strong linguistic grounding for the represented mathematical concepts.

ABSTRACT. Serious games are an attempt to leverage the inherent motivation in game-like scenarios for an educational application and to transpose the learning goals into real-world applications. Unfortunately, serious games are also very costly to develop and deploy. For very abstract domains like mathematics, already the representation of the knowledge involved becomes a problem.

We propose the FrameIT method that uses OMDoc/MMT theory graphs to represent and track the underlying knowledge in serious games. In this paper we report on an implementation and experiment that tests the method. We obtain a simple serious game by representing a ``word problem'' in OMDoc/MMT and connect the MMT API with a state-of-the-art game engine.

ABSTRACT. Most research pure mathematicians do not use computer theorem provers. One of the reasons for this: computer theorem provers cannot currently prove new theorems at research level in any of the main- stream areas of pure mathematical research, and proofs are the currency of pure mathematics. Note however that most research pure mathematicians did an undergraduate degree in mathematics, and in fact no computer theorem prover can prove—or even state—all the theorems in an undergraduate pure maths degree. These systems have been around for decades, and that is how far we have got – one would struggle to formalise the questions on most final year undergraduate pure mathematics courses, in any of the modern ITP systems.

We have to start somewhere if we want to get research mathematicians interested in these new technologies. I will talk about my vision for Lean’s mathematics library mathlib, currently over 50 percent of the way through formalising the proofs in the pure mathematics courses in Imperial College’s undergraduate mathematics degree.

ABSTRACT. Dependability analysis is an essential step in the design process of safety-critical systems, where the causes of failure and some other metrics, such as reliability, should be identified at an early design stage. The dynamic failure characteristics of real-world systems are usually captured by various dynamic dependability models, such as continuous time Markov chains (CTMCs), dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs). In order to conduct the formal dependability analysis of systems that exhibit dynamic failure behaviors, these models need to be captured formally. In this project paper, we describe recent developments towards this direction along with a roadmap on how to be able to develop a framework for formal reasoning support for DFTs, DRBDs and CTMCs in a higher-order-logic theorem prover.

ABSTRACT. Convex sets appear in various mathematical theories, and used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets in vector spaces, we formalize in Coq an intrinsic axiomatization of convex sets, namely convex spaces, based on an operation taking barycenters of points. A convex space corresponds to a specific type which does not refer to a surrounding vector space. This simplifies the definitions of functions on it. We show applications including the convexity of information-theoretic functions defined over types of distributions. We also show how convex spaces are embedded in conical spaces, which are abstract real cones, and use the embedding as an effective device to ease calculations.

ABSTRACT. Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discourse contains only sets, and hence every mathematical object must be a set. Consequently, in ZF, with the usual encoding of an ordered pair <a, b>, formulas like {a} ∈ <a, b> have truth values, and operations like P(<a, b>) have re- sults that are sets. Such ‘accidental theorems’ do not match how people think about the mathematics and also cause practical difficulties when using set theory in machine-assisted theorem proving. In contrast, in a number of proof assistants, mathematical objects and concepts can be built of type-theoretic stuff so that many mathematical objects can be, in essence, terms of an extended typed λ-calculus. However, dilemmas and frustration arise when formalizing mathematics in type theory. Motivated by problems of formalizing mathematics with (1) purely set-theoretic and (2) type-theoretic approaches, we explore an option with much of the flexibility of set theory and some of the useful features of type theory. We present ZFP: a modification of ZF that has ordered pairs as primitive, non-set objects. ZFP has a more natural and abstract axiomatic definition of ordered pairs free of any notion of representation. This paper presents axioms for ZFP, and a proof in ZF (machine-checked in Isabelle/ZF) of the existence of a model for ZFP, which implies that ZFP is consistent if ZF is. We discuss the approach used to add this abstraction barrier to ZF.

ABSTRACT. We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one.