ABSTRACT. The mathlib library is over 600K lines of code, all written in Lean 3. Lean 4 promises great extensibility, faster tactics, powerful and convenient macro programming – and no backward compatibility. As we have no desire to part with such a rich source of advanced formal mathematics, we are planning to port all of it to Lean 4. This might be the largest source-porting effort done in a theorem prover, so we're taking things slowly and investing heavily in high quality automated porting tool development. In this talk I will discuss our plans for how to translate all this source code to Lean 4 while preserving the quality standards and synthesizing the styles and tactics developed in mathlib with the new Lean 4 style.

ABSTRACT. An evaluable function computing the border array of a list in Isabelle/HOL is presented. The correctness of the function is verified in a straightforward lightweight manner, and it is applied for computation of other important properties of lists.

ABSTRACT. Many facts possess symmetrical counterparts that often require a separate formal proof, depending on the nature of the involved symmetry. We introduce a method in Isabelle/HOL which produces such a symmetrical fact for the list datatype and the symmetry induced by the list reversal mapping. The method is implemented as an attribute and its result is based on user-declared symmetry rules. Besides general rules, we provide rules that are aimed to be applied in the domain of Combinatorics on Words.

ABSTRACT. Rewriting theory is a well-established model of computation equivalent to the Turing machines, and the most well-known rewriting system is the $\lambda$-calculus. Confluence is an important and undecidable property related to the determinism of the computational process. Direct proofs of confluence are, in general, difficult to be done. Therefore, alternative characterizations of confluence can circumvent this difficulty for different contexts. This is the case of the so called Z property, which has been successfully used to prove confluence in several situations such as the $\lambda$-calculus with $\beta\eta$-reduction, extensions of the $\lambda$-calculus with explicit substitutions, the $\lambda\mu$-calculus, etc. In this work, we present a direct and constructive proof that the Z property implies confluence. In addition, we formalized our proof and an extension of the Z property, known as the Compositional Z, in the Coq proof assistant.

ABSTRACT. In this study, we analyze computer-aided inquiry-based mathematics learning. A Moodle plug-in associated with the dynamic geometry software CindyJS which can record finegrained log data of learners' manipulations on the web was used. Our previous study indicates that teacher intervention can make student's inquiry systematic and exhaustive by helping them build a semantic circuit across language, symbolism, and visual images which are relevant to the targeted concept. In this study, we try to validate the impact of this kind of teacher intervention by monitoring the log data of manipulations.

ABSTRACT. Traditionally, technical documents have been designed for print delivery in letter, A4, or similar sizes. Even the change to digital delivery using PDF has not changed the basic layout strategy and desktop screens can cope well. With the advent of mobile connected devices, it becomes natural to read technical documents (like everything else) e.g. on smartphones, which may demand other layout tradeoffs.

The document components most affected by this are diagrams and formulae, which -- unlike text -- cannot simply be reflowed to a new screen size. In this paper, we discuss an experimental study design that helps the investigation of the effect of linebreaking in mathematical formulae for reading efficiency using eye-tracking experiments.

ABSTRACT. Similarly to simple text, mathematical formulæ are a widely accepted language to represent ideas. Other representation of mathematical knowledge exist, e.g. in numeric or geometric forms. However, unlike text, mathematical objects are only transferrable (that is they can enter a transfer process) in limited and particular conditions, in part because encoding the formulæ is limited to encoding a graphical representation. An unsuccessful transfer leaves users with the task of transferring by redoing, retyping, or recreating the content.

Because automatic conversions may be working in many cases and because interoperable encoding and transfers could exist one day, this paper attempts to present scenarios of transfers of formulæ almost independently of what is doable currently. Inspired by the scenarios, a vision of interoperability could be built.

ABSTRACT. We present a new annotation tool, called MioGatto, to efficiently build large corpora for grounding math formulae. While in documents in science, technology, engineering, and mathematics, math identifiers can be used in multiple meanings in a single document, corpora with annotated coreference relations between identifiers are crucial for the grounding task. Using MioGatto, annotators can produce a list of math concepts for each document, associate one of the math concepts with each occurrence of math identifiers, and annotate the text span that is the source for grounding. In general, manual annotation of coreference relations is a very tough task, but this tool is specialized for building grounding corpora and can annotate them more efficiently than existing general-purpose annotation tools. The tool can be obtained from https://github.com/wtsnjp/MioGatto.

ABSTRACT. This paper presents RDF encodings for OpenMath objects and Content Dictionaries that allow mathematical objects and symbol definitions to be first-class citizens on the Web of Data.

ABSTRACT. Am OpenMath Content Dictionary with symbols for pattern matching of tree-like structures is presented. Furthermore, a mapping to RDF and SPARQL is introduced that allows to execute search queries against an OpenMath RDF representation.

ABSTRACT. Gambler’s ruin problem is an exciting application of probability theory which is generally used to analyze various practical scenarios like the security of bitcoin protocol. In this article, we provide a comprehensive analysis of the formalization of Gambler’s ruin problem. First, we present a comprehensive background and pen-and-paper calculation. Second, we summarize how to quantify the Gambler’s ruin problem and prepare all necessary intermediate conclusions. Third, we explain the difficulties we faced during the final formalization and analyze the strategies to overcome these barriers. Our final result: the recursive probability equation aims to establish the complete quantitative analysis of random walk and assist others in developing advanced probability analysis based on what we endeavor here.

ABSTRACT. The only squares in the Fibonacci sequence are 0, 1, and 144. We implemented a proof of this theorem in the Lean Theorem Prover. In this paper, we will discuss our methods as well as some implementation problems we faced and their solutions.

ABSTRACT. The aim of our work is to show, using the Mizar system that our techniques invented to formalize the unsolvability of Hilbert’s tenth problemin a Matiyasevich way, can be reused to prove that an assumption used byJulia Robinson demonstrates the same result independently. We present our formalization that the set of prime numbers is representable by a polynomial formula.

ABSTRACT. Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards developing a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways.

ABSTRACT. Sophize is a novel mathematics library and discussion platform with a mission to help our users find and organize mathematical proofs. We have extended the Markdown language to represent the connections between mathematical objects that exist across various sources of knowledge. Using the new language, we demonstrated an interactive interface that helps users explore mathematics content on the web. We also utilized this new language to create a novel communication system built specifically to aid mathematicians in solving problems collaboratively. This contribution sketches the basic ideas and provides links to some demos of the new functionality.

ABSTRACT. Within the MATh project, we develop explanation strategies to help first year students adapt to unacquainted workflows in university mathematics. These strategies are designed and implemented as sets of rules which are closely tied to the common practice in first year courses. In order to make the rules easily accessible to beginners it is useful to align them with commonly known concepts. Notably, the common experience with creating, continuing and reusing stories in varying situations turns out to be a promising starting point. We present a story-based approach for generating and structuring mathematical content within the MATh language and demonstrate that it entails various mathematical notions like theorem, set, function, theory and model. Due to this intimate relation between stories as structuring constructs and associated mathematical objects, the approach differs from other systems.

ABSTRACT. Extending the UFrameIT Framework, we propose an upgrade to the User Interface features that is directly built on the knowledge-based part, MMT. In the game engine, it suffices to interpret the output and visualize it accordingly, resulting in features that work generically and out of the box for all games built with UFrameIT. Initially, we were using fixed text descriptions and a static UI that created unnecessary mental load when players were trying to match between the abstract problem description and concrete game situations. To improve this, we introduce dynamic UI synchronization. We relate the progress of the player to the abstract formalized solution and give hints accordingly. These hints are generated via partial views; given a partial solution to the problem, MMT can check the dependencies and point towards the missing information. In the game, we can use this to highlight not yet assigned as well as even not yet existing facts in the game. This way, the player gets immediate feedback during the solution process.

ABSTRACT. While there are numerous linear algebra teaching tools, they tend to be focused on the basics, and not handle the more advanced aspects. This project aims to fill that gap, focusing specifically on methods like Strassen's fast matrix multiplication.

ABSTRACT. Next-generation mobility will be integrated, interconnected, and highly autonomous. One key challenge in mobility infrastructure management is ensuring safety while maintaining the required level of service quality. In this talk, I will highlight themes of my research related to proactive safety, road-user behavior, and formal verification. I will present recent advances in developing an automated framework for safety analysis. This research provides an insight into the failure mechanism that leads to road collisions and enables developing safety solutions for adaptive infrastructure management. I will discuss the role of formal methods, in particular temportal logic based run-time verification, in traffic safety diagnosis. The talk will also cover some examples and applications from real-world case studies.

ABSTRACT. Most of the engineering and physical systems are generally characterized by differential equations or difference equations based on their continuous-time and discrete-time dynamics, respectively. Moreover, these dynamical models are analyzed using transform methods to find out solutions of the differential/difference equations and prove their various properties, such as, transfer function, frequency response and stability. The Laplace and the Fourier transforms are used for analyzing systems exhibiting continuous dynamics. Whereas, the Discrete Fourier Transform (DFT) and the z-transform are their counterpart in the discrete time. The conventional techniques for performing the transform methods based analysis cannot provide an accurate analysis of the corresponding systems due to their inherent limitations. To overcome these limitations, formal methods, in particular, theorem proving, has been used, as a complementary technique, for analyzing systems based on transform methods and thus ascertain an accurate analysis. In this paper, we survey the developments in the use of higher-order-logic theorem proving for transform methods based analysis and overview the corresponding real world case studies from the avionics, medicine and transportation domains that have been analyzed based on these developments.

ABSTRACT. Power system protection plays a very significant role in the reliable operation of the power grid, by safeguarding the personnel, equipment, and property against any undesirable events. These protection systems are traditionally analyzed using computer simulation and physical testing. However, the sampling-based nature of these analysis techniques does not allow us to cover all the possible scenarios and thus the resulting protection systems may not guarantee complete protection. This fact can lead to partial or complete power loss/blackouts, which can have devastating consequences. Formal verification methods have been successfully used to overcome incomplete analysis issues in many domains of engineering. We believe that their introduction in the analysis of protection systems can lead to more reliable power grid operations. With this motivation, we propose to formally verify the correctness and reliability of the conventional and dual setting directional overcurrent relays. In this regard, we propose the development of the generic Markovian models of the conventional and dual setting directional overcurrent relays. To illustrate the effectiveness of the developed models a simple three bus distribution system network is analyzed to formally verify the efficiency and reliability of these models using PRISM, which is a probabilistic model checking tool. Furthermore, the failure and success probabilities of isolation of the faulty section are also determined.