Abstract is missing.
- Invited talk: Developments, Libraries and Automated Theorem ProversChad Brown. 2 [doi]
- Invited talk: On Differences in Proofs Between Intuitionistic and Classical LogicAleksy Schubert. 3 [doi]
- Tarski's Geometry and the Euclidean Plane in MizarAdam Grabowski, Roland Coghetto. 4-9 [doi]
- Formalization of the prime number theorem and Dirichlet's theoremMario Carneiro. 10-13 [doi]
- Topological Foundations for a Formal Theory of ManifoldsKarol Pak. 14-16 [doi]
- Registrations vs Redefinitions in MizarArtur Kornilowicz. 17-20 [doi]
- Linking to Compound Conditions in MizarAdam Naumowicz. 21-24 [doi]
- Towards Visual Type Theory as a Mathematical Tool and Mathematical User InterfaceLucius Schoenbaum. 26-41 [doi]
- Understanding Mathematical Expressions: An Eye-Tracking StudyAndrea Kohlhase, Michael Fürsich. 42-50 [doi]
- The plain text trap when copying mathematical formulaePaul Libbrecht, Matija Lokar. 50-55 [doi]
- Proposal for Coexistence of Mathematical Handwritten and Keyboard Input in a WYSIWYG Expression EditorJuan Lao-Tebar, Francisco Alvaro, Daniel Marques. 56-65 [doi]
- KAT: an Annotation Tool for STEM DocumentsTom Wiesing, Felix Schmoll. 66-72 [doi]
- Notation-based SemantificationIon Toloaca, Michael Kohlhase. 73-81 [doi]
- Lucas-Interpretation from Users' PerspectiveWalther Neuper. 83-89 [doi]
- Rigor of TP in Educational Engineering SoftwareWalther Neuper. 90-95 [doi]
- Automated theorem proving for elementary geometryMarek Janasz. 97 [doi]
- Knowledge Management across Formal LibrariesDennis Müller. 98-101 [doi]
- Augmenting Mathematical Formulae for More Effective Querying & PresentationMoritz Schubotz. 102-103 [doi]
- Design and development of a tool based on Coq to write and format mathematical proofsThéo Zimmermann. 104-105 [doi]
- swMATH - Challenges, Next Steps, and OutlookHagen Chrapary, Wolfgang Dalitz, Wolfram Sperber. 107-116 [doi]
- Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System MizarHiroyuki Okazaki, Yuichi Futa. 117-131 [doi]
- A Smooth Transition to Modern mathoid-based Math Rendering in Wikipedia with Automatic Visual Regression TestingMoritz Schubotz, Alan P. Sexton. 132-145 [doi]
- Getting the units rightMoritz Schubotz, David Veenhuis, Howard S. Cohl. 146-156 [doi]
- Lemma Extraction Criteria Based on Properties of Theorem StatementsKarol Pak. 158-171 [doi]
- The impact of proof steps sequence on proof readability - experimental settingKarol Pak, Aleksy Schubert. 172-186 [doi]
- Models for MetamathMario Carneiro. 187-203 [doi]
- A first step towards automated conjecture-making in higher arithmetic geometryAndreas Holmstrom. 204-218 [doi]
- Initial Experiments with Statistical Conjecturing over Large Formal CorporaThibault Gauthier, Cezary Kaliszyk, Josef Urban. 219-228 [doi]
- A Standard for Aligning Mathematical ConceptsCezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe. 229-244 [doi]
- FrameIT Reloaded: Serious Math Games from Modular Math OntologiesDenis Rochau, Michael Kohlhase, Dennis Müller. 245-259 [doi]