You must enable JavaScript to use this site
  • 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

    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

  • News

Privacy policy and legal information
Last modified: March 26 2024 06:58:16 CET