CICM-WS 2021
Workshop Papers of the 14th Conference on Intelligent Computer Mathematics (CICM 2021)

Table of Contents

• Preface
  summary: There were 39 papers submitted for peer-review to this workshop. Out of these, 28 regular papers were accepted for this volume.

Formal Mathematics for Mathematicians (FMM) (Short Papers)

• FMM Preface
  Jasmin Blanchette, Adam Naumowicz
• Computing the Border Array in Isabelle/HOL (short paper)
  Stepan Holub
• Producing Symmetrical Facts for lIsts induced by the List Reversal Mapping in Isabelle/HOL (short paper)
  Martin Raška, Štěpán Starosta
• Formalization of Gambler’s Ruin Problem (short paper)
  Zibo Yang
• Formalizing Fibonacci Squares (short paper)
  Muhammad Harun Ali Khan
• Formalization of Prime Representing Polynomial in Mizar (short paper)
  Karol Pąk
• Verified Optimization (work in progress)
  Alexander Bentkamp, Jeremy Avigad
• Elements of Differential Geometry in Lean: A Report for Mathematicians (short paper)
  Anthony Bordg, Nicolo Cavalleri
• A Web Platform for Hosting the Mizar Mathematical Library (short paper)
  Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki
• Scalar actions in Lean's mathlib (short paper)
  Eric Wieser
• Automatically Generalizing Theorems Using Typeclasses (short paper)
  Alex J. Best
• Formalizing the Gromov-Hausdorff space
  Sebastien Gouezel

2nd Workshop on Formal Verification of Physical Systems (FVPS 2021)

• FVPS Preface
  Osman Hasan
• Formalization of Transform Methods in Higher-order Logic: A Survey (short paper)
  Muhammad Ahmed, Adnan Rashid

13th MathUI Workshop 2021 - Mathematical User Interaction

• MathUI Preface
  Andrea Kohlhase
• A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
  Andrea Kohlhase, Michael Kohlhase
• Story Based Content Structuring in MATh
  Michael Junk, Sebastian Sahli
• Monitoring the Impact of Teacher's Intervention in Inquiry-Based Mathematics Learning with the use of Dynamic Geometry
  Takeo Noda, Takahiro Nakahara, Masataka Kaneko
• MioGatto: A Math Identifier-oriented Grounding Annotation Tool
  Takuto Asakura, Yusuke Miyao, Akiko Aizawa, Michael Kohlhase
• Sophize Markdown and Collaboration Interface
  Abhishek Chugh
• Dynamic User Interfaces via Incremental Knowledge Management
  Richard Marcus, Michael Kohlhase, Navid Roux, John Schihada

NatFoM 2021 - Workshop on Natural Formal Mathematics

• NatFoM Preface
  Peter Koepke, Dennis Müller
• Natural Typesetting of Naproche Formalizations in LaTeX (short paper)
  Peter Koepke, Tim Lichtnau, Jonas Lippert
• Formal Mathematics for the Masses (short paper)
  William M. Farmer
• System Description: sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents (short paper)
  Dennis Müller, Michael Kohlhase, Jan Frederik Schaefer
• Semantic parsing of geometry statements using supervised machine learning on synthetic data
  Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar

31th OpenMath Workshop

• OpenMath Preface
  James H. Davenport, Michael Kohlhase
• OpenMath-RDF: RDF Encodings for OpenMath Objects and Content Dictionaries
  Ken Wenzel
• Pattern Matching for Mathematical Expressions with OpenMath (short paper)
  Ken Wenzel

CICM 2021 Doctoral Programme

• Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs - Extended Abstract (short paper)
  Fabian Huch
• Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics - Extended Abstract
  Jonas Betzendahl
• Deep Learning for Automated Theorem Proving - Extended Abstract
  Stanisław Purgał
• Develop a Mathematical E-Dictionary and Test it - Extended Abstract
  Theresa Kruse

CICM 2021 Informal Track

• Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
  Zoltán Kovács, Robert Vajda