Abstract is missing.
- A Promising Path Towards Autoformalization and General Artificial IntelligenceChristian Szegedy. 3-20 [doi]
- Formal Adventures in Convex and Conical SpacesReynald Affeldt, Jacques Garrigue, Takafumi Saikawa. 23-38 [doi]
- Towards a Heterogeneous Query Language for Mathematical KnowledgeKatja Bercic, Michael Kohlhase, Florian Rabe. 39-54 [doi]
- Leveraging the Information Contained in Theory PresentationsJacques Carette, William M. Farmer, Yasmine Sharoda. 55-70 [doi]
- Metamath Zero: Designing a Theorem Prover ProverMario M. Carneiro. 71-88 [doi]
- Adding an Abstraction Barrier to ZF Set TheoryCiarán Dunne, J. B. Wells, Fairouz Kamareddine. 89-104 [doi]
- A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem ProvingYassmeen Elderhalli, Osman Hasan, Sofiène Tahar. 105-122 [doi]
- Induction with Generalization in Superposition ReasoningMárton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov. 123-137 [doi]
- A Survey of Languages for Formalizing MathematicsCezary Kaliszyk, Florian Rabe. 138-156 [doi]
- Edu: A Linguistically Grounded Educational Mathematical OntologyAlexander Kirillovich, Olga Nevzorova, Marina Falileeva, Evgeny Lipachev, Liliana Shakirova. 157-172 [doi]
- FrameIT: Detangling Knowledge Management from Game Design in Serious GamesMichael Kohlhase, Benjamin Bösl, Richard Marcus, Dennis Müller 0001, Denis Rochau, Navid Roux, John Schihada, Marc Stamminger. 173-189 [doi]
- Formalizing Graph Trail Properties in Isabelle/HOLLaura Kovács, Hanna Lachnitt, Stefan Szeider. 190-205 [doi]
- Representing Structural Language Features in Formal Meta-languagesDennis Müller 0001, Florian Rabe, Colin Rothgang, Michael Kohlhase. 206-221 [doi]
- Formally Verifying Proofs for Algebraic Identities of MatricesLeonard Schmitz, Viktor Levandovskyy. 222-236 [doi]
- AutoMSC: Automatic Assignment of Mathematics Subject Classification LabelsMoritz Schubotz, Philipp Scharpf, Olaf Teschke, Andreas Kühnemund, Corinna Breitinger, Bela Gipp. 237-250 [doi]
- Maintaining a Library of Formal MathematicsFloris van Doorn, Gabriel Ebner, Robert Y. Lewis. 251-267 [doi]
- The Tactician - A Seamless, Interactive Tactic Learner and Prover for CoqLasse Blaauwbroek, Josef Urban, Herman Geuvers. 271-277 [doi]
- Tree Neural Networks in HOL4Thibault Gauthier. 278-283 [doi]
- Interpreting Mathematical Texts in Naproche-SADAdrian De Lon, Peter Koepke, Anton Lorenzen. 284-289 [doi]
- TGView3D: A System for 3-Dimensional Visualization of Theory GraphsRichard Marcus, Michael Kohlhase, Florian Rabe. 290-296 [doi]
- Simple Dataset for Proof Method Recommendation in Isabelle/HOLYutaka Nagashima. 297-302 [doi]
- Dataset Description: Formalization of Elementary Number Theory in MizarAdam Naumowicz. 303-308 [doi]
- Guiding Inferences in Connection Tableau by Recurrent Neural NetworksBartosz Piotrowski, Josef Urban. 309-314 [doi]
- First Neural Conjecturing Datasets and ExperimentsJosef Urban, Jan Jakubuv. 315-323 [doi]
- A Contextual and Labeled Math-Dataset Derived from NIST's DLMFAbdou Youssef, Bruce R. Miller. 324-330 [doi]