Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 colocated with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 2529, 2016
Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, Martin Suda (Editors)
 Anthology ID:
 2016.cikm_workshop2016fm4m
 Year:
 2016
 Venue:
 cikm_workshop
 Publisher:
 CEURWS.org
 URL:
 https://ceurws.org/Vol1785
 DBLP:
 conf/cikm/2016fm4m
Invited talk: Developments, Libraries and Automated Theorem Provers
Chad Brown
Invited talk: On Differences in Proofs Between Intuitionistic and Classical Logic
Aleksy Schubert
Tarski's Geometry and the Euclidean Plane in Mizar
Adam Grabowski

Roland Coghetto
Formalization of the prime number theorem and Dirichlet's theorem
Mario Carneiro
Topological Foundations for a Formal Theory of Manifolds
Karol Pak
Registrations vs Redefinitions in Mizar
Artur Kornilowicz
Linking to Compound Conditions in Mizar
Adam Naumowicz
Towards Visual Type Theory as a Mathematical Tool and Mathematical User Interface
Lucius Schoenbaum
Understanding Mathematical Expressions: An EyeTracking Study
Andrea Kohlhase

Michael Fürsich
The plain text trap when copying mathematical formulae
Paul Libbrecht

Matija Lokar
Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression Editor
Juan LaoTebar

Francisco Alvaro

Daniel Marques
KAT: an Annotation Tool for STEM Documents
Tom Wiesing

Felix Schmoll
Notationbased Semantification
Ion Toloaca

Michael Kohlhase
LucasInterpretation from Users' Perspective
Walther Neuper
Rigor of TP in Educational Engineering Software
Walther Neuper
Automated theorem proving for elementary geometry
Marek Janasz
Knowledge Management across Formal Libraries
Dennis Müller
Augmenting Mathematical Formulae for More Effective Querying & Presentation
Moritz Schubotz
Design and development of a tool based on Coq to write and format mathematical proofs
Théo Zimmermann
swMATH  Challenges, Next Steps, and Outlook
Hagen Chrapary

Wolfgang Dalitz

Wolfram Sperber
Formalization of Polynomially Bounded and Negligible Functions Using the ComputerAided ProofChecking System Mizar
Hiroyuki Okazaki

Yuichi Futa
A Smooth Transition to Modern mathoidbased Math Rendering in Wikipedia with Automatic Visual Regression Testing
Moritz Schubotz

Alan P. Sexton
Getting the units right
Moritz Schubotz

David Veenhuis

Howard S. Cohl
Lemma Extraction Criteria Based on Properties of Theorem Statements
Karol Pak
The impact of proof steps sequence on proof readability  experimental setting
Karol Pak

Aleksy Schubert
Models for Metamath
Mario Carneiro
A first step towards automated conjecturemaking in higher arithmetic geometry
Andreas Holmstrom
Initial Experiments with Statistical Conjecturing over Large Formal Corpora
Thibault Gauthier

Cezary Kaliszyk

Josef Urban
A Standard for Aligning Mathematical Concepts
Cezary Kaliszyk

Michael Kohlhase

Dennis Müller

Florian Rabe
FrameIT Reloaded: Serious Math Games from Modular Math Ontologies
Denis Rochau

Michael Kohlhase

Dennis Müller