Abstract is missing.
- Interaction with Formal Mathematical Documents in Isabelle/PIDEMakarius Wenzel. 1-15 [doi]
- Beginners' Quest to Formalize Mathematics: A Feasibility Study in IsabelleJonas Bayer, Marco David, Abhik Pal, Benedikt Stock. 16-27 [doi]
- Towards a Unified Mathematical Data Infrastructure: Database and Interface GenerationKatja Bercic, Michael Kohlhase, Florian Rabe. 28-43 [doi]
- A Tale of Two Set TheoriesChad E. Brown, Karol Pak. 44-60 [doi]
- Relational Data Across Mathematical LibrariesAndrea Condoluci, Michael Kohlhase, Dennis Müller 0001, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel. 61-76 [doi]
- Variadic Equational MatchingBesik Dundua, Temur Kutsia, Mircea Marin. 77-92 [doi]
- Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic DecompositionMatthew England, Dorian Florescu. 93-108 [doi]
- Towards Specifying Symbolic ComputationJacques Carette, William M. Farmer. 109-124 [doi]
- Lemma Discovery for Induction - A SurveyMoa Johansson. 125-139 [doi]
- Experiments on Automatic Inclusion of Some Non-degeneracy Conditions Among the Hypotheses in Locus Equation ComputationsZoltán Kovács, Pavel Pech. 140-154 [doi]
- Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOLAlexander Maletzky. 155-170 [doi]
- The Coq Library as a Theory GraphDennis Müller 0001, Florian Rabe, Claudio Sacerdoti Coen. 171-186 [doi]
- BNF-Style Notation as It Is Actually UsedDee Quinlan, Joe B. Wells, Fairouz Kamareddine. 187-204 [doi]
- MMTTeX: Connecting Content and Narration-Oriented Document FormatsFlorian Rabe. 205-210 [doi]
- Diagram Combinators in MMTFlorian Rabe, Yasmine Sharoda. 211-226 [doi]
- Inspection and Selection of RepresentationsDaniel Raggi, Aaron Stockdill, Mateja Jamnik, Grecia Garcia Garcia, Holly E. A. Sutherland, Peter C.-H. Cheng. 227-242 [doi]
- A Plugin to Export Coq Libraries to XMLClaudio Sacerdoti Coen. 243-257 [doi]
- Forms of Plagiarism in Digital Mathematical LibrariesMoritz Schubotz, Olaf Teschke, Vincent Stange, Norman Meuschke, Bela Gipp. 258-274 [doi]
- Integrating Semantic Mathematical Documents and Dynamic NotebooksKai Amann, Michael Kohlhase, Florian Rabe, Tom Wiesing. 275-290 [doi]
- Explorations into the Use of Word Embedding in Math Search and Math SemanticsAbdou Youssef, Bruce R. Miller. 291-305 [doi]