ABSTRACT. In this paper we present the Cambridge Isabelle Parallel Corpus (CIPC), a parallel corpus of mathematical facts and their proofs expressed in both natural language and in Isabelle/HOL. Our corpus could be useful in many tasks related to machine learning in theorem proving, such as autoformalisation. We also discuss challenges and requirements associated with constructing the CIPC, identified during a pilot study, that are distinct from parallel corpora for natural language (\textit{e.g.} French and English). At the time of writing, the CIPC contains over 500 facts (definitions, lemmata, theorems), with parallel proof scripts included for 18 of those entries. We envisage the CIPC to be a living corpus since the optimal number of parallel proof scripts for autoformalisation is a major unanswered research question.

ABSTRACT. The On-line Encyclopedia of Integer Sequences (OEIS) is an important resource for casual and professional mathematicians. Applications range from being able to access information about a specific graph problem while researching the lifetime of multicomponent models in engineering to treating the search for new sequences as an entertaining puzzle. The database is well-structured and rich in mathematical content but is informal in nature, so interaction with the database is restricted to humans supported by basic search services. In this paper we provide the result of semantifying -- i.e. recovering machine-actionable representations -- the OEIS data as an open dataset organized along the tetrapod model of mathematical knowledge. We hope that this dataset will trigger the development of novel user interfaces, derived data, connections to other mathematical data sets and libraries, and advance knowledge management services by the mathematical community.

ABSTRACT. Bringing out the potential of interactive theorem provers requires efficient mathematical foundations. The current release of the natural language proof assistant Naproche has become sufficiently stable to allow a broader and principled approach towards libraries of basic mathematical material. We present Naproche's new ontology of objects, classes, maps, etc. and two foundational libraries about basic set theory and number theory. These foundations are then used, e.g., in a formalization of the Cantor–Schröder–Bernstein theorem.

ABSTRACT. Naproche is a proof assistant for mathematical texts written in controlled natural language. The input is translated to first order logic and then checked using standard reasoning procedures and automatic theorem provers. Naproche ships on the Isabelle Platform and we expect larger formalizations to be developed in this environment. However, we seek to lower the barrier of entry even further, so that a general mathematical audience can try Naproche easily. Our web-interface can be used on any system within seconds and performs comparably to the desktop distribution. That makes it a feasible alternative for use in short lecture courses and conference presentations.

ABSTRACT. We contribute a Python client for the Isabelle server, which gives researchers and students using Python as their primary programming language an opportunity to communicate with the Isabelle server through TCP directly from a Python script. Such an approach helps avoid the complexities of integrating the existing Python script with languages used for Isabelle development (ML and Scala). We also describe new features that appeared since the announcement of the first version of the client a year ago. Finally, we give examples of the client's applications in research and education and discuss known limitations and possible directions for future development.