| Vol-1785 urn:nbn:de:0074-1785-8 Copyright © 2017 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.

# CICM-WS-WIP 2016
Workshop and Work in Progress Papers at CICM 2016

## • FMM - Formal Mathematics for Mathematicians
• The 11th Workshop on Mathematical User Interfaces (MathUI)
• The 2016 Workshop on Theorem proving components for Educational software (ThEdu)
• The Work in Progress Section of the MKM track of CICM 2016
• The Work in Progress Section of the DML track of CICM 2016
• The CICM 2016 Doctoral Program

### Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016
co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016)

### Bialystok, Poland, July 25-29, 2016.

Edited by

### Michael Kohlhase, FAU Erlangen Nürnberg (Joint volume editor and CICM program chair)
Andrea Kohlhase, Hochschule Neu-Ulm (MathUI editor)
Paul Libbrecht, German Institute for international Educational Research, Frankfurt, (MathUI editor)
Bruce Miller, NIST (MKM WiP editor)
Adam Naumowicz, University of Bialystok (FM4M editor and CICM organizer)
Walther Neuper, Graz University of Technology (ThEdu editor)
Pedro Quaresma, University of Coimbra (ThEdu editor)
Frank Tompa, University of Waterloo (DML WiP editor)
Martin Suda, TU Wien (Doctoral Program editor)

## Table of Contents

- Preface

### FM4M - Formal Mathematics for Mathematicians

- Preface
- Invited Talk: Developments, Libraries and Automated Theorem Provers 2
  Chad Brown
- Invited Talk: On Differences in Proofs Between Intuitionistic and Classical Logic 3
  Aleksy Schubert
- Tarski's Geometry and the Euclidean Plane in Mizar 4-9
  Adam Grabowski, Roland Coghetto
- Formalization of the Prime Number Theorem and Dirichlet's Theorem 10-13
  Mario Carneiro
- Topological Foundations for a Formal Theory of Manifolds 14-16
  Karol Pąk
- Registrations vs. Redefinitions in Mizar 17-20
  Artur Korniłowicz
- Linking to Compound Conditions in Mizar 21-24
  Adam Naumowicz

### The 11th Workshop on Mathematical User Interfaces (MathUI)

- Preface
- Towards Visual Type Theory as a Mathematical Tool and Mathematical User Interface 26-41
  Lucius Schoenbaum
- Understanding Mathematical Expressions: An Eye-Tracking Study 42-50
  Andrea Kohlhase, Michael Fürsich
- The Plain Text Trap when Copying Mathematical Formulae 50-55
  Paul Libbrecht, Matija Lokar
- Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor 56-65
  Juan Lao-Tebar, Francisco Alvaro, Daniel Marques
- KAT: an Annotation Tool for STEM Documents 66-72
  Tom Wiesing, Felix Schmoll
- Notation-based Semantification 73-81
  Ion Toloaca, Michael Kohlhase

### The 2016 Workshop on Theorem proving components for Educational software (ThEdu)

- Preface
- Lucas-Interpretation from Users' Perspective 83-89
  Walther Neuper
- Rigor of TP in Educational Engineering Software 90-95
  Walther Neuper

### The CICM 2016 Doctoral Program

- Preface
- Automated Theorem Proving for Elementary Geometry 97-97
  Marek Janasz
- Knowledge Management across Formal Libraries 98-101
  Dennis Müller
- Augmenting Mathematical Formulae for More Effective Querying & Presentation 102-103
  Moritz Schubotz
- Design and Development of a Tool Based on Coq to Write and Format Mathematical Proofs 104-105
  Théo Zimmermann

### The Work in Progress Section of the DML track of CICM 2016

- Preface
- swMATH - Challenges, Next Steps, and Outlook 107-116
  Hagen Chrapary, Wolfgang Dalitz, and Wolfram Sperber
- Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar 117-131
  Hiroyuki Okazaki, and Yuichi Futa
- A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression Testing 132-145
  Moritz Schubotz and Alan P. Sexton
- Getting the Units Right 146-156
  Moritz Schubotz, David Veenhuis, and Howard S. Cohl

### The Work in Progress Section of the MKM track of CICM 2016

- Preface
- Lemma Extraction Criteria Based on Properties of Theorem Statements 158-171
  Karol Pak
- The Impact of Proof Steps Sequence on Proof Readability - Experimental Setting 172-186
  Karol Pak, Aleksy Schubert
- Models for Metamath 187-203
  Mario Carneiro
- A First Step Towards Automated Conjecture-Making in Higher Arithmetic geometry 204-218
  Andreas Holmstrom
- Initial Experiments with Statistical Conjecturing over Large Formal Corpora 219-228
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban
- A Standard for Aligning Mathematical Concepts 229-244
  Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe
- FrameIT Reloaded: Serious Math Games from Modular Math Ontologies 245-259
  Denis Rochau, Michael Kohlhase, Dennis Müller

2017-01-22: submitted by Michael Kohlhase metadata incl. bibliographic data published under Creative Commons CC0
2017-01-22: published on CEUR-WS.org |valid HTML5|