List of Events

Invited Talks

• [I1] John Harrison. TBA
• [I2] Claudio Sacerdoti Coen. Towards Extensible Algorithmic Mathematical Knowledge (Slides)
• [I3] Nicolas Thierry. Infrastructure for generic code in SageMath: categories, axioms, constructions (Slides)

Regular papers

• [R5] Adam Naumowicz and Radosław Piliszek. Accessing the Mizar Library with a Weakly Strict Mizar Parser
• [R8] William Farmer. Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Slides)
• [R19] Chad Brown and Josef Urban. Extracting Higher-Order Goals from the Mizar Mathematical Library (Slides)
• [R21] Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry and Tom Wiesing. Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach
• [R39] Waqar Ahmed, Osman Hasan and Sofiene Tahar. Formal Dependability Modeling and Analysis: A Survey (Slides)
• [R18] Jan Jakubuv and Josef Urban. Extending E Prover with Similarity Based Clause Selection Strategies
• [R42] Artur Kornilowicz. Enhancement of Mizar Texts with Transitivity Property of Predicates
• [R4] Alexander Maletzky. Mathematical Theory Exploration in Theorema: Reduction Rings
• [R11] Ken'Ichi Kuga, Manabu Hagiwara and Mitsuharu Yamamoto. Formalization of Bing's shrinking method in geometric topology
• [R31] Erika Ábrahám, Bernd Becker, James H. Davenport and Pascal Fontaine. SC-square: Satisfiability Checking meets Symbolic Computation
• [R36] Muhammad Qasim, Osman Hasan, Maissa Elleuch and Sofiene Tahar. Formalization of Normal Random Variables in HOL (Slides)
• [R32] Olaf Teschke and Fabian Müller. Progress of self-archiving within the DML corpus, with a view toward community dynamics

Work in progress

• [W1] Mario Carneiro. Models for Metamath (Slides)
• [W44] Andreas Holmstrom. A first step towards automated conjecture-making in higher arithmetic geometry
• [W47] Karol Pąk and Aleksy Schubert. The impact of proof steps sequence on proof readability – experimental setting
• [W23] Thibault Gauthier, Cezary Kaliszyk and Josef Urban. Initial Experiments with Statistical Conjecturing over Large Formal Corpora
• [W33] Karol Pąk. Lemma Extraction Criteria Based on Properties of Theorem Statements
• [W24] Cezary Kaliszyk, Michael Kohlhase, Dennis Müller and Florian Rabe. A Standard for Aligning Mathematical Concepts
• [W50] Denis Rochau, Michael Kohlhase and Dennis Müller. FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
• [W10] Wolfram Sperber, Hagen Chrapary and Wolfgang Dalitz. swMATH - challenges, next steps, and outlook (Slides)
• [W38] Hiroyuki Okazaki and Yuichi Futa. Formalization of Polynomially Bounded and Negligible Functions using the Computer-Aided Proof-Checking System Mizar
• [W45] Moritz Schubotz, David Veenhuis and Howard Cohl. Getting the units right (Slides)
• [W48] Moritz Schubotz and Alan Sexton. A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing (Slides)

Doctoral Programme

• [DP1] Marek Janasz. Automated theorem proving for elementary geometry
• [DP2] Dennis Müller. Knowledge Management across Formal Libraries
• [DP3] Moritz Schubotz. Augmenting Mathematical Formulae for More Effective Querying & Presentation (Slides)
• [DP4] Théo Zimmermann. Design and development of a tool based on Coq to write and format mathematical proofs

Workshop Mathematical User Interfaces (MathUI)

• [M1] Lucius Schoenbaum. Towards Visual Type Theory as Mathematical Tool and Mathematical User Interface
• [M2] Andrea Kohlhase and Michael Fürsich. Understanding Mathematical Expressions: An Eye-Tracking Study
• [M3] Paul Libbrecht and Matija Lokar. The plain text trap when copying mathematical formulae
• [M4] Juan Lao-Tebar, Francisco Alvaro and Daniel Marqus. Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
• [M5] Tom Wiesing and Felix Schmoll. KAT: an Annotation Tool for STEM Documents
• [M6] Ion Toloaca and Michael Kohlhase. Notation-based Semantification

OpenMath Workshop

• [O0] Michael Kohlhase. The 29th OpenMath Workshop, Agenda/Planning
• [O1] Tom Wiesing. An Overview over SCSCP
• [O2] Bruce Miller. Drafting DLMF Content Dictionaries
• [O3] Moritz Schubotz. Implicit Content Dictionaries in the NIST Digital Repository of Mathematical Formulae (Slides)
• [O4] Moritz Schubotz. Displaying formulae in Wikimedias central structured data storage Wikidata (Slides)
• [O5] Michael Kohlhase. Towards OpenMath 2.1 or 3; Issues and Criteria
• [O6] Michael Kohlhase. Sequence Variables in OpenMath

Workshop Formal Mathematics for Mathematicians (FM4M)

• [F1] Chad Brown. Invited talk: Developments, Libraries and Automated Theorem Provers (Slides)
• [F2] Adam Grabowski. Tarski's geometry and Euclidean plane in Mizar
• [F3] Mario Carneiro. Formalization of the prime number theorem and Dirichlet's theorem (Slides)
• [F4] Karol Pąk. Topological Foundations for a Formal Theory of Manifolds
• [F5] Artur Korniłowicz. Registrations vs Redefinitions in Mizar
• [F6] Aleksy Schubert. Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic
• [F7] Adam Naumowicz. Linking to Compound Conditions in Mizar

Workshop on computer Theorem proving components for Educational software (ThEdu)

• [T1] Walther Neuper. Lucas-Interpretation from Users’ Perspective (Slides)
• [T2] Walther Neuper. Rigor of TP in Educational Engineering Software (Slides)

Tutorials

• [MMT1] Florian Rabe, Mihnea Iancu, Dennis Müller. Language Design in MMT (Slides)
• [MMT2] Florian Rabe, Mihnea Iancu, Dennis Müller. Application Design with MMT (Slides)